blob: 920c87e0b847dcd2d740af54032e0beb0e141c91 (
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
|
-------------------- Prog0.jen --------------------
Jennisys, Copyright (c) 2011, Microsoft.
---------- Given Jennisys program ----------
class C {
var a: seq[int]
var x: int
constructor Init()
{
}
method Update(d)
{
x := x + 1
{
nested := statement
yes := sirrie
}
x.f := (12 + true)[8000 := 0 <= n]
}
method Query() returns (r)
requires r
requires *
requires r.r.s
requires a[i]
requires a[i := 58]
requires hello
requires (hello + goodbye) - soonyousoon
requires 0 <= r
{
}
method ManyParams(x: bool, y) returns (r, s: set[MyClass], t)
{
}
}
model C {
var x: int
frame
xyz
invariant
x <= x
}
code C {
}
----------
-------------------- ExtensibleArray.jen --------------------
Jennisys, Copyright (c) 2011, Microsoft.
---------- Given Jennisys program ----------
class ExtensibleArray[T] {
var Contents: seq[T]
constructor Init()
{
Contents := []
}
method Get(i) returns (t)
requires 0 <= i
requires i < |Contents|
{
t := Contents[i]
}
method Set(i, t)
requires 0 <= i
requires i < |Contents|
{
Contents := Contents[i := t]
}
method Append(t)
{
Contents := Contents + [t]
}
}
model ExtensibleArray[T] {
var elements: array[T]
var more: ExtensibleArray[array[T]]
var length: int
var M: int
frame
(elements * more) * more.Contents[*]
invariant
elements != null
elements.Length = 256
more = null ==> M = 0
more != null ==> |more.Contents| != 0 && M = 256 * |more.Contents|
0 <= length
length <= M + 256
more != null ==> M < length
length = |Contents|
forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256]
forall i :: M <= i && i < length ==> Contents[i] = elements[i - M]
}
----------
|