Test/test2/LambdaOldExpressions.bpl


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

var b: bool;


procedure p0();
  requires b;
  modifies b;
  ensures (lambda x: bool :: old(b))[true];
  ensures !(lambda x: bool :: b)[true];

implementation p0()
{
    b := !b;
    assert (lambda x: bool :: old(b))[true];
    assert !(lambda x: bool :: b)[true];
}


procedure p1();
  requires !b;
  modifies b;
  ensures (lambda x: bool :: old(b))[true];  // error

implementation p1()
{
    b := !b;
    assert !(lambda x: bool :: old(b))[true];
}


procedure p2();
  requires b;
  modifies b;
  ensures (lambda x: bool :: old(b) != b)[true];

implementation p2()
{
    b := !b;
    assert (lambda x: bool :: old(b) != b)[true];
}