Theory IMP2
theory IMP2
imports "automation/IMP2_VCG" "automation/IMP2_Specification"
begin
section ‹IMP2 Setup›
lemmas [deriv_unfolds] = Params_def Inline_def AssignIdx_retv_def ArrayCpy_retv_def
section ‹Ad-Hoc Regression Tests›
experiment begin
lemma upd_idxSame[named_ss vcg_bb]: "f(i:=a,i:=b) = f (i:=b)" by auto
lemmas [named_ss vcg_bb] = triv_forall_equality
declare [[eta_contract = false ]]
program_spec (partial) p2
assumes "n>0"
ensures "n=0"
defines ‹while (n>0) @invariant ‹n≥0› { if (n+1>1) {
n=n-1;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
G1=n; G2=n; G3=n; n=G1; n=G2; n=G3;
skip
} }›
apply vcg
by auto
program_spec p2'
assumes "n>0"
ensures "n=0"
defines ‹while (n>0) @variant ‹n› @invariant ‹n≥0› { n=n-1 }›
apply vcg
by auto
program_spec p2''
assumes "n>0"
ensures "n=0"
defines ‹while (n>0) @relation ‹measure nat› @variant ‹n› @invariant ‹n≥0› { n=n-1 }›
apply vcg
by auto
program_spec p3
assumes "True"
ensures "n = n⇩0 ∧ N=42"
defines ‹
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope n = 0;
scope {n = 0}; N=42
›
apply vcg
by auto
end
subsection ‹More Regression Tests›
experiment begin
lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib
program_spec exp_count_up1
assumes "0≤n"
ensures "a = 2^nat n⇩0"
defines ‹
a = 1;
c = 0;
while (c<n)
@variant ‹n-c›
@invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
{
a=2*a;
c=c+1
}
›
apply vcg
by (auto simp: algebra_simps nat_distribs)
program_spec exp_count_up1'
assumes "0≤n"
ensures "a = 2^nat n⇩0"
defines ‹
a = 1;
c = 0;
while (c<n)
@variant ‹n-c›
@invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
{
a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a;
c=c+1
}
›
apply vcg
by (auto simp: algebra_simps nat_distribs)
program_spec exp_count_up
assumes "0≤n"
ensures "a = 2^nat n⇩0"
defines ‹
a = 1;
c = 0;
while (c<n)
@variant ‹n-c›
@invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
{
a=2*a;
{
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a; a=2*a;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2; a=a / 2;
skip
};
c=c+1
}
›
apply vcg
apply (all ‹simp?›)
apply (auto simp: algebra_simps nat_distribs)
done
program_spec exp_count_up3
assumes "0≤n"
ensures "a = 2^nat n⇩0"
defines ‹
a = 1;
c = 0;
while (c<n)
@variant ‹n-c›
@invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
{
a=2*a;
{
a=a+a; a=a+a; a=a+a; a = a/8;
a=a+a; a=a+a; a=a+a; a = a/8;
a=a+a; a=a+a; a=a+a; a = a/8;
a=a+a; a = a/2;
skip
};
c=c+1
}
›
apply vcg
apply (all ‹simp?›)
apply (auto simp: algebra_simps nat_distribs)
done
end
experiment
begin
lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib
procedure_spec exp_count_up (n) returns a
assumes "0≤n"
ensures "a = 2^nat n⇩0"
defines ‹
a = 1;
c = 0;
while (c<n)
@variant ‹n-c›
@invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
{
a=2*a;
c=c+1
}
›
apply vcg
by (auto simp: algebra_simps nat_distribs)
program_spec use_exp
assumes "0≤n"
ensures ‹n = 2^(2^nat n⇩0)›
defines ‹
n = exp_count_up(n);
n = exp_count_up(n)
›
apply vcg
by auto
procedure_spec add3 (a, b, c) returns r
assumes "a≥0 ∧b≥0 ∧c≥0"
ensures "r = a⇩0+b⇩0+c⇩0"
defines ‹
r = a+b+c
›
apply vcg
by auto
procedure_spec use_add3 (a, b) returns r
assumes "a≥0 ∧ b≥0"
ensures "r = 2*(a⇩0+b⇩0+b⇩0)"
defines ‹
r1 = add3(a, b, b);
r2 = add3(a, b, b);
r = r1+r2
›
apply vcg
by auto
procedure_spec divmod (a,b) returns (c,d)
assumes "b≠0"
ensures "c = a⇩0 div b⇩0 ∧ d = a⇩0 mod b⇩0"
defines ‹
c = a / b;
d = a mod b
›
apply vcg
by auto
procedure_spec use_divmod (a,b) returns r
assumes "b≠0"
ensures "r = a⇩0"
defines ‹
(d,m) = divmod (a,b);
r = d*b + m
›
apply vcg
by simp
end
experiment
begin
lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib
procedure_spec exp_count_up (n) returns a
assumes "0≤n"
ensures "a = 2^nat n⇩0"
defines ‹
a = 1;
c = 0;
while (c<n)
@variant ‹n-c›
@invariant ‹0≤c ∧ c≤n ∧ a=2^nat c›
{
a=2*a;
c=c+1
}
›
apply vcg
by (auto simp: algebra_simps nat_distribs)
program_spec use_exp
assumes "0≤n"
ensures ‹n = 2^(2^nat n⇩0)›
defines ‹
n = exp_count_up(n);
n = exp_count_up(n)
›
apply vcg
by auto
text ‹Deriving big-step semantics›
schematic_goal
"Map.empty: (use_exp,<''n'':=λ_. 2>) ⇒ ?s"
"?s ''G_ret_1'' 0 = 16"
unfolding use_exp_def exp_count_up_def
apply big_step []
by bs_simp
schematic_goal
"Map.empty: (use_exp,<''n'':=λ_. 2>) ⇒ ?s"
"?s ''G_ret_1'' 0 = 16"
unfolding use_exp_def exp_count_up_def
apply (big_step'+) []
by bs_simp
procedure_spec add3 (a, b, c) returns r
assumes "a≥0 ∧b≥0 ∧c≥0"
ensures "r = a⇩0+b⇩0+c⇩0"
defines ‹
r = a+b+c
›
apply vcg
by auto
procedure_spec use_add3 (a, b) returns r
assumes "a≥0 ∧ b≥0"
ensures "r = 2*(a⇩0+b⇩0+b⇩0)"
defines ‹
r1 = add3(a, b, b);
r2 = add3(a, b, b);
r = r1+r2
›
apply vcg
by auto
procedure_spec no_param () returns r
assumes "True"
ensures "r = 42"
defines ‹r = 42›
by vcg_cs
procedure_spec foobar (a) returns r
assumes ‹a≥0›
ensures "r=84+a⇩0"
defines ‹
r1 = no_param();
add3(a, a, r1);
r2 = add3(a, r1, r1);
r = r2
›
apply vcg_cs
done
end
experiment begin
lemma [named_ss vcg_bb]: "BB_PROTECT True" by (auto simp: BB_PROTECT_def)
procedure_spec add (a,b) returns r assumes True ensures "r=a⇩0+b⇩0" defines ‹r = a + b› by vcg_cs
procedure_spec test (a) returns r assumes True ensures "r = a⇩0" defines ‹
x1 = add(a,a);
x2 = add(a,a);
x3 = add (x1-x2, a);
x1 = add(a,a);
x2 = add(a,a);
x3 = add (x1-x2, a);
x1 = add(a,a);
x2 = add(a,a);
x3 = add (x1-x2, a);
x1 = add(a,a);
x2 = add(a,a);
x3 = add (x1-x2, a);
x1 = add(a,a);
x2 = add(a,a);
x3 = add (x1-x2, a);
x1 = add(a,a);
x2 = add(a,a);
x3 = add (x1-x2, a);
r = x3
›
apply vcg
by auto
end
experiment begin
lemmas nat_distribs = nat_add_distrib nat_diff_distrib Suc_diff_le nat_mult_distrib nat_div_distrib
recursive_spec
relation ‹measure nat›
foo (a) returns b
assumes "a≥0"
ensures "b = 2^nat a⇩0"
variant "a"
defines ‹
if (a==0) b=1
else {
b = rec foo (a-1);
b = 2 * b
}
›
thm vcg_specs
apply vcg
apply (auto simp: nat_distribs algebra_simps)
by (metis (full_types) Suc_pred le0 le_less nat_0_iff not_le power_Suc)
thm foo_spec
recursive_spec
odd (a) returns b
assumes "a≥0"
ensures "b≠0 ⟷ odd a⇩0"
variant "a"
defines ‹
if (a==0) b=0
else {
b = rec even (a-1)
}
›
and
even (a) returns b
assumes ‹a≥0›
ensures "b≠0 ⟷ even a⇩0"
variant "a"
defines ‹
if (a==0) b=1
else {
b = rec odd (a-1)
}
›
apply vcg
by auto
thm even_spec odd_spec
end
end