1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11(*<*)
12theory Chapter2_HoareHeap
13imports "AutoCorres.AutoCorres"
14begin
15
16external_file "mult_by_add.c"
17(*>*)
18
19section  {* More Complex Functions with AutoCorres *}
20
21text {*
22
23  In the previous section we saw how to use the C-Parser and AutoCorres
24  to prove properties about some very simple C programs.
25
26  Real life C programs tend to be far more complex however; they
27  read and write to local variables, have loops and use pointers to
28  access the heap. In this section we will look at some simple programs
29  which use loops and access the heap to show how AutoCorres can
30  allow such constructs to be reasoned about.
31
32*}
33
34subsection {* A simple loop: \texttt{mult\_by\_add} *}
35
36text {*
37
38  Our C function \texttt{mult\_by\_add} implements a multiply operation
39  by successive additions:
40
41\lstinputlisting[language=C, firstline=15]{../../mult_by_add.c}
42
43  We start by translating the program using the C parser and AutoCorres,
44  and entering the generated locale \texttt{mult\_by\_add}.
45*}
46
47install_C_file "mult_by_add.c"
48autocorres [ts_rules = nondet] "mult_by_add.c"
49(*<*)
50context mult_by_add begin
51(*>*)
52
53text {*
54  The C parser produces the SIMPL output as follows:
55*}
56
57thm mult_by_add_body_def
58text {* @{thm [display] mult_by_add_body_def} *}
59
60text {*
61  Which is abstracted by AutoCorres to the following:
62*}
63
64thm mult_by_add'_def
65text {* @{thm [display] mult_by_add'_def } *}
66
67text {*
68
69  In this case AutoCorres has abstracted \texttt{mult\_by\_add} into a
70  \emph{monadic} form. Monads are a pattern frequently used in
71  functional programming to represent imperative-style control-flow; an
72  in-depth introduction to monads can be found elsewhere.
73
74  The monads used by AutoCorres in this example is a
75  \emph{non-deterministic state monad}; program state is implicitly
76  passed between each statement, and results of computations may produce
77  more than one (or possibly zero) results\footnote{Non-determinism
78  becomes useful when modelling hardware, for example, where the exact
79  results of the hardware cannot be determined ahead of time.}.
80*}
81  (* FIXME : probably describe below in further detail. *)
82text {*
83  The bulk of @{term "mult_by_add'"} is wrapped inside the @{term
84  "whileLoop"} \emph{monad combinator}, which is really just a fancy way
85  of describing the method used by AutoCorres to encode (potentially
86  non-terminating) loops using monads.
87
88  If we want to describe the behaviour of this program, we can use
89  Hoare logic as follows:
90
91    @{term [display] "\<lbrace> P \<rbrace> mult_by_add' a b \<lbrace> Q \<rbrace>"}
92
93  This predicate states that, assuming @{term "P"} holds on the initial
94  program state, if we execute @{term "mult_by_add' a b"}, then
95  @{term "Q"} will hold on the final state of the program.
96
97  There are a few details: while @{term "P"} has type
98  @{typ "'s \<Rightarrow> bool"} (i.e., takes a state and returns true if
99  it satisifies the precondition), @{term "Q"} has an additional
100  parameter @{typ "'r \<Rightarrow> 's \<Rightarrow> bool"}. The additional parameter
101  @{typ "'r"} is the \emph{return value} of the function; so, in
102  our \texttt{mult\_by\_add'} example, it will be the result of
103  the multiplication.
104
105  For example one useful property to prove on our program would
106  be:
107
108    @{term [display] "\<lbrace> \<lambda>s. True \<rbrace> mult_by_add' a b \<lbrace> \<lambda>r s. r = a * b \<rbrace>"}
109
110  That is, for all possible input states, our \texttt{mult\_by\_add'}
111  function returns the product of @{term "a"} and @{term "b"}.
112
113  Unfortunately, this is not sufficient. As mentioned in the previous
114  section, AutoCorres produces a theorem for each function it abstracts
115  stating that, \emph{assuming the function does not fail}, then the
116  generated function is a valid abstraction of the concrete function.
117  Thus, if we wish to reason about our concrete C function, we must
118  also show non-failure on the abstract program. This can be done
119  using the predicate @{term "no_fail"} as follows:
120
121    @{term [display] "\<And>a b. no_fail (\<lambda>s. True) (mult_by_add' a b)"}
122
123  Here @{term "\<lambda>s. True"} is the precondition on the input state.
124
125  Instead of proving our Hoare triple and @{term no_fail} separately,
126  we can prove them together using the ``valid no fail'' framework
127  as follows:
128
129    @{thm [display] validNF_def}
130
131  Our proof of @{term mult_by_add'} could then proceed as follows:
132
133*}
134
135lemma mult_by_add_correct:
136    "\<lbrace> \<lambda>s. True \<rbrace> mult_by_add' a b \<lbrace> \<lambda>r s. r = a * b \<rbrace>!"
137  txt {* Unfold abstracted definition *}
138  apply (unfold mult_by_add'_def)
139  txt {* Annotate the loop with an invariant and a measure. *}
140  apply (subst whileLoop_add_inv
141    [where I="\<lambda>(a', result) s. result = (a - a') * b"
142        and M="\<lambda>((a', result), s). a'"] )
143  txt {* Run the ``weakest precondition'' tool \texttt{wp}. *}
144  apply wp
145  txt {* Solve the program correctness goals. *}
146     apply (simp add: field_simps)
147    apply unat_arith
148   apply (auto simp: field_simps not_less)
149  done
150
151(* FIXME: Update the following explanation. *)
152text {*
153  The proof is straight-forward, but uses a few different techniques:
154  The first is that we annotate the loop with a loop invariant and a
155  measure, using the rule @{thm whileLoop_add_inv}. We then run the
156  \texttt{wp} tool which applys a large set of
157  \emph{weakest precondition} rules on the program\footnote{This set of
158  rules includes a rule which can handle annotated @{term whileLoop}
159  terms, but will not attempt to process @{term whileLoop} terms without
160  annotations.}. We finially discharge the remaining subgoals left from
161  the \texttt{wp} tool using \texttt{auto}, and our proof is complete.
162
163  In the next section, we will look at how we can use AutoCorres to
164  verify a C program that reads and writes to the heap.
165
166*}
167
168(*<*)
169end
170end
171(*>*)
172