summaryrefslogtreecommitdiff
path: root/Test/dafny0/Calculations.dfy
blob: 8ef361393f48787f47e032939e6c5da0ba699f65 (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
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
	}
}

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]
}