1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7theory Plus 8imports 9 "AutoCorres.AutoCorres" 10begin 11 12external_file "plus.c" 13install_C_file "plus.c" 14 15autocorres [ ts_force nondet = plus2 ] "plus.c" 16 17context plus begin 18 19(* 3 + 2 should be 5 *) 20lemma "plus' 3 2 = 5" 21 unfolding plus'_def 22 by eval 23 24(* plus does what it says on the box *) 25lemma plus_correct: "plus' a b = a + b" 26 unfolding plus'_def 27 apply (rule refl) 28 done 29 30(* Compare pre-lifting to post-lifting *) 31thm plus_global_addresses.plus2_body_def 32thm plus2'_def 33 34(* plus2 does what it says on the box *) 35lemma plus2_correct: "\<lbrace>\<lambda>s. True\<rbrace> plus2' a b \<lbrace> \<lambda>r s. r = a + b\<rbrace>" 36 unfolding plus2'_def 37 apply (subst whileLoop_add_inv 38 [where I="\<lambda>(a', b') s. a' + b' = a + b" 39 and M="\<lambda>((a', b'), s). b'"]) 40 apply (wp, auto simp: not_less) 41 done 42 43(* plus2 does what it says on plus's box *) 44lemma plus2_is_plus: "\<lbrace> \<lambda>s. True \<rbrace> plus2' a b \<lbrace> \<lambda>r s. r = plus' a b \<rbrace>" 45 unfolding plus'_def 46 apply (simp add:plus2_correct) 47 done 48 49(* Prove plus2 with no failure *) 50lemma plus2_valid:"\<lbrace> \<lambda>s. True \<rbrace> plus2' a b \<lbrace> \<lambda>r s. r = a + b \<rbrace>!" 51 unfolding plus2'_def 52 apply (subst whileLoop_add_inv 53 [where I="\<lambda>(a', b') s. a' + b' = a + b" 54 and M="\<lambda>((a', b'), s). b'"]) 55 apply wp 56 apply clarsimp 57 apply unat_arith 58 apply clarsimp 59 apply unat_arith 60 apply clarsimp 61 done 62 63end 64 65end 66