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