summaryrefslogtreecommitdiff
path: root/Test/dafny0/Calculations.dfy
blob: f10d2e45f1960852e7281f125790420ff1595a62 (plain)
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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
method CalcTest0(s: seq<int>) {
  calc {
    s[0]; // error: ill-formed line
  }
  
  calc {
    2;
    { assert s[0] == 1; } // error: ill-formed hint
    1 + 1;
  }
  
  if (|s| > 0) {
    calc {
      s[0]; // OK: well-formed in this context
      <= { assert s[0] == s[0]; }
      s[0];
    }
  }
  assume forall x :: x in s ==> x >= 0;
  calc {
    0 < |s|;
  ==>  { assert s[0] >= 0; }  // OK: well-formed after previous line
    s[0] >= 0;                // OK: well-formed after previous line
  <==> { assert s[0] >= 0; }  // OK: well-formed when the previous line is well-formed
    s[0] > 0 || s[0] == 0;    // OK: well-formed when the previous line is well-formed
  }
  
  calc { // same as the last one, but well-formedness is checked in reverse order
    s[0] + 1 > 0;
  <==>
    s[0] >= 0;
  <== { assert s[0] >= 0; }
    0 < |s|;
  }  
}

method CalcTest1(x: int, y: int) {
  calc {
    x + y;
    { assume x == 0; }
    y;
  }
  assert x == 0; // OK: follows from x + y == y;
}

method CalcTest2(x: int, y: int) {
  calc {
    x + y;
    { assume x == 0; }
    y + x;
  }
  assert x == 0; // error: even though assumed above, is not exported by the calculation
}

// calc expression:
function CalcTest3(s: seq<int>): int {
  calc < {
    0;
    { assume |s| == 5; }
    |s|;
  }
  s[0]
}

// dangling hints:
method CalcTest4(s: seq<int>) 
  requires forall n | n in s :: n > 0;
{
  calc {
    1 + 1;
    { assert 1 + 1 == 2; }
  }
  calc {
    2;
    { assert s[0] > 0; } // error: ill-formed hint
  }
  calc {
    |s| > 0;
  ==> { assert s[0] > 0; } // okay
  }
  
}

// ------------- tests for the pretty printer -------------

lemma CalcPrinting()
{
  calc < {
    2;
  <= { SubLemma(); }
    3;
    5;
  < { assert 5 < 6 <= 5+1; SubLemma(); assert 6 < 7; }
    7;
    11;
    { SubLemma(); } // dangling hint
  }
  calc < {
    13;
  }
  calc {
    17;
  == { SubLemma(); }  // dangling hint, following operator
  }
  calc <= {
    19;
  <=
    { SubLemma(); }
    { assert 19 + 23 == 42; }
    calc { 811; }
    { assert 42 < 100; }
    23;
    { calc < {
      71; { assert 71 % 19 != 0; } 73;
    } }
    29;
    calc < {
      311; 313; 331;
    }
    31;
  }
  calc {
  }
}

lemma SubLemma()