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