Theory Quickstart_Guide
section ‹Quickstart Guide›
theory Quickstart_Guide
imports "../IMP2"
begin
subsection ‹Introductory Examples›
text ‹IMP2 provides commands to define program snippets or procedures together with their specification.›
procedure_spec div_ab (a,b) returns c
assumes ‹b≠0›
ensures ‹c=a⇩0 div b⇩0›
defines ‹c = a/b›
by vcg_cs
text ‹The specification consists of the signature (name, parameters, return variables),
precondition, postcondition, and program text.›
text ‹
➧[Signature] The procedure name and variable names must be valid Isabelle names.
The ‹returns› declaration is optional, by default, nothing is returned.
Multiple values can be returned by ‹returns (x⇩1,...,x⇩n)›.
➧[Precondition] An Isabelle formula. Parameter names are valid variables.
➧[Postcondition] An Isabelle formula over the return variables, and parameter names suffixed with ‹⇩0›.
➧[Program Text] The procedure body, in a C-like syntax.
›
text ‹The @{command procedure_spec} command will open a proof to show that the program satisfies the specification.
The default way of discharging this goal is by using IMP2's verification condition generator, followed by
manual discharging of the generated VCs as necessary.
Note that the @{method vcg_cs} method will apply @{method clarsimp} to all generated VCs, which, in our case,
already solves them. You can use @{method vcg} to get the raw VCs.
›
text ‹If the VCs have been discharged, @{command procedure_spec} adds prologue and epilogue code
for parameter passing, defines a constant for the procedure, and lifts the pre- and postcondition
over the constant definition.
›
thm div_ab_spec
thm div_ab_def
text ‹The final theorem has the form \<^term>‹HT_mods π vs P c Q›,
where ‹π› is an arbitrary procedure environment,
‹vs› is a syntactic approximation of the (global) variables modified by the procedure,
‹P,Q› are the pre- and postcondition, lifted over the parameter passing code,
and ‹c› is the defined constant for the procedure.
The precondition is a function \<^typ>‹state⇒bool›. It starts with a series of variable bindings
that map program variables to logical variables,
followed by precondition that was specified, wrapped in a \<^const>‹BB_PROTECT› constant,
which serves as a tag for the VCG, and is defined as the identity (@{thm BB_PROTECT_def}).
The final theorem is declared to the VCG, such that the specification will be
used automatically for calls to this procedure.
›
procedure_spec use_div_ab(a) returns r assumes ‹a≠0› ensures ‹r=1› defines ‹r = div_ab(a,a)› by vcg_cs
subsubsection ‹Variant and Invariant Annotations›
text ‹Loops must be annotated with variants and invariants.›
procedure_spec mult_ab(a,b) returns c assumes ‹True› ensures "c=a⇩0*b⇩0"
defines ‹
if (a<0) {a = -a; b = -b};
c=0;
while (a>0)
@variant ‹a›
@invariant ‹0≤a ∧ a≤¦a⇩0¦ ∧ c = ( ¦a⇩0¦ - a) * b⇩0 * sgn a⇩0›
{
c=c+b;
a=a-1
}
›
apply vcg_cs
apply (auto simp: algebra_simps)
done
text ‹The variant and invariant can use the program variables.
Variables suffixed with ‹⇩0› refer to the values of parameters at the start of the program.
The variant must be an expression of type \<^typ>‹int›, which decreases with every loop iteration and is always ‹≥0›.
❙‹Pitfall›: If the variant has a more general type, e.g., \<^typ>‹'a›, an explicit type annotation
must be added. Otherwise, you'll get an ugly error message directly from Isabelle's type checker!
›
subsubsection ‹Recursive Procedures›
text ‹IMP2 supports mutually recursive procedures. All procedures of a mutually recursive specification
have to be specified and proved simultaneously.
Each procedure has to be annotated with a variant over the parameters.
On a recursive call, the variant of the callee for the arguments must be smaller than the
variant of the caller (for its initial arguments).
Recursive invocations inside the specification have to be tagged by the ‹rec› keyword.
›
recursive_spec
odd_imp(n) returns b assumes "n≥0" ensures ‹b≠0 ⟷ odd n⇩0› variant ‹n›
defines ‹if (n==0) b=0 else b=rec even_imp(n-1)›
and
even_imp(n) returns b assumes "n≥0" ensures ‹b≠0 ⟷ even n⇩0› variant ‹n›
defines ‹if (n==0) b=1 else b=rec odd_imp(n-1)›
by vcg_cs
text ‹After proving the VCs, constants are defined as usual, and the correctness theorems
are lifted and declared to the VCG for future use.›
thm odd_imp_spec even_imp_spec
subsection ‹The VCG›
text ‹The VCG is designed to produce human-readable VCs.
It takes care of presenting the VCs with reasonable variable names,
and a location information from where a VC originates.
›
procedure_spec mult_ab'(a,b) returns c assumes ‹True› ensures "c=a⇩0*b⇩0"
defines ‹
if (a<0) {a = -a; b = -b};
c=0;
while (a>0)
@variant ‹a›
@invariant ‹0≤a ∧ a≤¦a⇩0¦ ∧ c = ( ¦a⇩0¦ - a) * b⇩0 * sgn a⇩0›
{
c=c+b;
a=a-1
}
›
apply vcg
text ‹The \<^term>‹¶xxx› tags in the premises give a hint to the origin of each VC.
Moreover, the variable names are derived from the actual variable names in the program.›
by (auto simp: algebra_simps)
subsection ‹Advanced Features›
subsubsection ‹Custom Termination Relations›
text ‹Both for loops and recursive procedures, a custom termination relation can be specified, with the
‹relation› annotation. The variant must be a function into the domain of this relation.
❙‹Pitfall›: You have to ensure, by type annotations, that the most general type of
the relation and variant fit together. Otherwise, ugly low-level errors will be the result.
›
procedure_spec mult_ab''(a,b) returns c assumes ‹True› ensures "c=a⇩0*b⇩0"
defines ‹
if (a<0) {a = -a; b = -b};
c=0;
while (a>0)
@relation ‹measure nat›
@variant ‹a›
@invariant ‹0≤a ∧ a≤¦a⇩0¦ ∧ c = ( ¦a⇩0¦ - a) * b⇩0 * sgn a⇩0›
{
c=c+b;
a=a-1
}
›
by vcg_cs (auto simp: algebra_simps)
recursive_spec relation ‹measure nat›
odd_imp'(n) returns b assumes "n≥0" ensures ‹b≠0 ⟷ odd n⇩0› variant ‹n›
defines ‹if (n==0) b=0 else b=rec even_imp'(n-1)›
and
even_imp'(n) returns b assumes "n≥0" ensures ‹b≠0 ⟷ even n⇩0› variant ‹n›
defines ‹if (n==0) b=1 else b=rec odd_imp'(n-1)›
by vcg_cs
subsubsection ‹Partial Correctness›
text ‹IMP2 supports partial correctness proofs only for while-loops.
Recursive procedures must always be proved totally correct⁋‹Adding partial correctness for recursion
is possible, however, compared to total correctness, showing that the prove rule is sound
requires some effort that we have not (yet) invested.››
procedure_spec (partial) nonterminating() returns a assumes True ensures ‹a=0› defines
‹while (a≠0) @invariant ‹True›
a=a-1›
by vcg_cs
subsubsection ‹Arrays›
text ‹IMP2 provides one-dimensional arrays of integers, which are indexed by integers.
Arrays do not have to be declared or allocated. By default, every index maps to zero.
In the specifications, arrays are modeled as functions of type \<^typ>‹int⇒int›.
›
lemma array_sum_aux: "l⇩0≤l ⟹ {l⇩0..<l + 1} = insert l {l⇩0..<l}" for l⇩0 l :: int by auto
procedure_spec array_sum(a,l,h) returns s assumes "l≤h" ensures ‹s = (∑i=l⇩0..<h⇩0. a⇩0 i)› defines
‹ s=0;
while (l<h)
@variant ‹h-l›
@invariant ‹l⇩0≤l ∧ l≤h ∧ s = (∑i=l⇩0..<l. a i)›
{ s = s+a[l]; l=l+1 } ›
apply vcg_cs
apply (simp add: array_sum_aux)
done
subsection ‹Proving Techniques›
text ‹This section contains a small collection of techniques to tackle large proofs.›
subsubsection ‹Auxiliary Lemmas›
text ‹Prove auxiliary lemmas, and try to keep the actual proof of the specification small.
As a rule of thumb: All VCs that cannot be solved by a simple @{method auto} invocation
should go to an auxiliary lemma.
The auxiliary lemma may either re-state the whole VC, or only prove the ``essence'' of the VC,
such that the rest of its proof becomes automatic again.
See the @{const array_sum} program above for an example or the latter case.
❙‹Pitfall› When extracting auxiliary lemmas, it is too easy to get too general types, which
may render the lemmas unprovable. As an example, omitting the explicit type constraints
from @{thm [source] "array_sum_aux"} will yield an unprovable statement.
›
subsubsection ‹Inlining›
text ‹More complex procedure bodies can be modularized by either splitting them into
multiple procedures, or using inlining and @{command program_spec} to explicitly prove a
specification for a part of a program. Cf.\ the insertion sort example for the latter technique. ›
subsubsection ‹Functional Refinement›
text ‹
Sometimes, it makes sense to state the algorithm functionally first, and then prove that
the implementation behaves like the functional program, and, separately, that the functional
program is correct. Cf.\ the mergesort example.
›
subsubsection ‹Data Refinement›
text ‹Moreover, it sometimes makes sense to abstract the concrete variables to abstract types,
over which the algorithm is then specified. For example, an array ‹a› with a range ‹l..<h› can
be understood as a list. Or an array can be used as a bitvector set.
Cf.\ the mergesort and dedup examples. ›
subsection ‹Troubleshooting›
text ‹We list a few common problems and their solutions here›
subsubsection ‹Invalid Variables in Annotations›
text ‹Undeclared variables in annotations are highlighted, however, no warning or error is produced.
Usually, the generated VCs will not be provable. The most common mistake is to
forget the ‹⇩0› suffix when referring to parameter values in (in)variants and postconditions.›
text ‹Note the highlighting of unused variables in the following example›
procedure_spec foo(x1,x2) returns y assumes "x1>x2+x3" ensures "y = x1⇩0+x2" defines ‹
y=0;
while (x1>0)
@variant ‹y + x3›
@invariant ‹y>x3›
{
x1=x2
}
›
oops
text ‹Even worse, if the most general type of an annotation becomes too general,
as free variables have type \<^typ>‹'a› by default, you will see an internal type error.
Try replacing the variant or invariant with a free variable in the above example.
›
subsubsection ‹Wrong Annotations›
text ‹For total correctness, you must annotate a loop variant and invariant.
For partial correctness, you must annotate an invariant, but ❙‹no variant›.
When not following this rule, the VCG will get stuck in an internal state
›
procedure_spec (partial) foo () assumes True ensures True defines ‹
while (n>0) @variant ‹n› @invariant ‹True›
{ n=n-1 }
›
apply vcg
oops
subsubsection ‹Calls to Undefined Procedures›
text ‹Calling an undefined procedure usually results in a type error, as the procedure
name gets interpreted as an Isabelle term, e.g., either it refers to an existing constant,
or is interpreted as a free variable›
subsection ‹Missing Features›
text ‹This is an (incomplete) list of missing features.›
subsubsection ‹Elaborate Warnings and Errors›
text ‹Currently, the IMP2 tools only produce minimal error and warning messages.
Quite often, the user sees the raw error message as produced by Isabelle unfiltered,
including all internal details of the tools.
›
subsubsection ‹Static Type Checking›
text ‹We do no static type checking at all.
In particular, we do not check, nor does our semantic enforce, that procedures are called
with the same number of arguments as they were declared.
Programs that violate this convention may even have provable properties, as argument
and parameter passing is modeled as macros on top of the semantics, and the semantics has no
notion of failure.
›
subsubsection ‹Structure Types›
text ‹Every variable is an integer arrays. Plain integer variables are implemented as
macros on top of this, by referring to index ‹0›.
The most urgent addition to increase usability would be record types.
With them, we could model encapsulation and data refinement more explicitly, by
collecting all parts of a data structure in a single (record-typed) variable.
An easy way of adding record types would follow a similar route as arrays,
modeling values of variables as a recursive tree-structured datatype.
@{theory_text [display] ‹datatype val = PRIM int | STRUCT "fname ⇒ val" | ARRAY "int ⇒ val"›}
However, for modeling the semantics, we most likely want to introduce an explicit error state,
to distinguish type errors (e.g. accessing a record field of an integer value) from nontermination.
›
subsubsection ‹Function Calls as Expressions›
text ‹Currently, function calls are modeled as statements, and thus, cannot be nested into
expressions. Doing so would require to simultaneously specify the semantics of
commands and expressions, which makes things more complex.
As the language is intended to be simple, we have not done this.
›
subsubsection ‹Ghost Variables›
text ‹Ghost variables are a valuable tool for expressing (data) refinement,
and hinting the VCG towards the abstract algorithm structure.
We believe that we can add ghost variables with annotations on top of the VCG,
without actually changing the program semantics.
›
subsubsection ‹Concurrency›
text ‹IMP2 is a single threaded language.
We have no current plans to add concurrency, as this would greatly complicate both the
semantics and the VCG, which is contrary to the goal of a simple language for educational
purposes.
›
subsubsection ‹Pointers and Memory›
text ‹Adding pointers and memory allocation to IMP2 is theoretically possible, but, again,
this would complicate the semantics and the VCG.
However, as the author has some experience in VCGs using separation logic, he might actually
add pointers and memory allocation to IMP2 in the near future.
›
end