Strata/StrataTest/DL/Imperative/Examples.lean at main · strata-org/Strata · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
/-
  Copyright Strata Contributors

  SPDX-License-Identifier: Apache-2.0 OR MIT
-/

import StrataTest.DL.Imperative.Verify

---------------------------------------------------------------------
namespace Strata

---------------------------------------------------------------------
def testProgram1 : Program :=
#strata
program ArithPrograms;
  init x : num := 0;
  x := 1;
  havoc x;
  assert [x_eq_1]: (x == 1); // error
#end

/--
info: Label: x_eq_1
Property : assert
Assumptions: ⏎
Obligation: ($__x0 : Num) = 1
Metadata: ⏎


Obligation x_eq_1: could not be proved!

Result: Obligation: x_eq_1
Result: failed
Counterexample: ($__x0, 0)
---
info:
Obligation: x_eq_1
Result: failed
Counterexample: ($__x0, 0)
-/
#guard_msgs in
#eval Strata.ArithPrograms.verify testProgram1

---------------------------------------------------------------------

def testProgram2 : Program :=
#strata
program ArithPrograms;
  init x : num := 0;
  x := 1;
  init y : num := 0;
  assert [x_eq_y]: (x == (y + 1 * 1));
#end

/--
info: Label: x_eq_y
Property : assert
Assumptions: ⏎
Obligation: true
Metadata: ⏎

---
info:
Obligation: x_eq_y
Result: verified
-/
#guard_msgs in
#eval Strata.ArithPrograms.verify testProgram2

---------------------------------------------------------------------

def testProgram3 : Program :=
#strata
program ArithPrograms;
  var x : num;
  var b : bool;
  b := (2 * x == x + x);
  assert [double_x_lemma]: (b);
#end

/--
info: Label: double_x_lemma
Property : assert
Assumptions: ⏎
Obligation: 2 × (init_x_0 : Num) = (init_x_0 : Num) + (init_x_0 : Num)
Metadata: ⏎

---
info:
Obligation: double_x_lemma
Result: verified
-/
#guard_msgs in
#eval Strata.ArithPrograms.verify testProgram3

---------------------------------------------------------------------