-
Notifications
You must be signed in to change notification settings - Fork 47
/
Copy pathapplying-twice-quantified-lhs.vpr
85 lines (63 loc) · 2.47 KB
/
applying-twice-quantified-lhs.vpr
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
field f: Int
method test13a(xs: Seq[Ref])
requires forall x: Ref :: x in xs ==> acc(x.f)
requires |xs| >= 1
{
xs[0].f := 0
var some: Ref := xs[0]
package (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)
some.f := 1
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
some.f := 2
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
//:: ExpectedOutput(assert.failed:assertion.false)
assert false
}
method test13b(xs: Seq[Ref])
requires forall x: Ref :: x in xs ==> acc(x.f)
requires |xs| >= 1
{
xs[0].f := 0
var some: Ref := xs[0]
package (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)
some.f := 1
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
some.f := 2
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) --* acc(some.f)) in true
//:: ExpectedOutput(assert.failed:assertion.false)
assert false
var completed: Seq[Ref] := Seq(some)
assert forall z: Ref :: z in completed ==> (forall x: Ref :: x in xs ==> acc(x.f)) --* acc(z.f)
}
method test13c(xs: Seq[Ref], y: Ref)
requires forall x: Ref :: x in xs ==> acc(x.f)
requires |xs| >= 1
requires acc(y.f)
{
xs[0].f := 0
var some: Ref := xs[0]
package (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)
some.f := 1
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
some.f := 2
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
//:: ExpectedOutput(assert.failed:assertion.false)
assert false
}
method test13d(xs: Seq[Ref], y: Ref)
requires forall x: Ref :: x in xs ==> acc(x.f)
requires |xs| >= 1
requires acc(y.f)
{
xs[0].f := 0
var some: Ref := xs[0]
package (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)
some.f := 1
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
some.f := 2
assert applying ((forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(some.f) && acc(y.f)) in true
//:: ExpectedOutput(assert.failed:assertion.false)
assert false
var completed: Seq[Ref] := Seq(some)
assert forall z: Ref :: z in completed ==> (forall x: Ref :: x in xs ==> acc(x.f)) && acc(y.f) --* acc(z.f) && acc(y.f)
}