blob: 142d18f282dc53d1c7d79ff1bd68357954b27985 (
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
|
// RUN: %boogie -noinfer "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// aren't these cool!
var m: []int;
var p: <a>[]a;
type ref;
const null: ref;
procedure P()
requires m[] == 5;
modifies m;
modifies p;
ensures m[] == 30;
ensures p[] == null;
{
m[] := 12;
p[] := 12;
p[] := true;
assert p[] == m[];
assert p[];
m := m[:= 30];
p := p[:=null];
}
procedure Q()
modifies m;
{
assert m[] == 5; // error
m[] := 30;
assert m[] == 5; // error
}
procedure R()
modifies p;
{
assert p[] < 3; // error
}
// ----
type Field a;
type HeapType = <a>[ref, Field a]a;
const F0: Field int;
const F1: Field bool;
const alloc: Field bool;
var Heap: HeapType;
procedure FrameCondition(this: ref)
modifies Heap;
ensures (forall<a> o: ref, f: Field a ::
Heap[o,f] == old(Heap)[o,f] ||
!old(Heap)[o,alloc] ||
(o == this && f == F0) ||
(o == this && f == F1)
);
{
}
|
