diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-07 18:33:22 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-07 18:33:22 -0700 |
| commit | 7ae15e4ab4aa4e63257ed2e426fe2a0efa35de21 (patch) | |
| tree | 28ce98153ac5b86a07feeaf0488462f43eee83ed /Test/jennisys0 | |
| parent | 4c4750f967d56c02bb55b2f485ddc466f1b33a58 (diff) | |
Jennisys: Parse and print
Diffstat (limited to 'Test/jennisys0')
| -rw-r--r-- | Test/jennisys0/Answer | 93 | ||||
| -rw-r--r-- | Test/jennisys0/ExtensibleArray.jen | 47 | ||||
| -rw-r--r-- | Test/jennisys0/Prog0.jen | 34 | ||||
| -rw-r--r-- | Test/jennisys0/runtest.bat | 10 |
4 files changed, 184 insertions, 0 deletions
diff --git a/Test/jennisys0/Answer b/Test/jennisys0/Answer new file mode 100644 index 00000000..64099079 --- /dev/null +++ b/Test/jennisys0/Answer @@ -0,0 +1,93 @@ +
+-------------------- 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 && (i < |Contents|))
+ {
+ t := Contents[i]
+ }
+ method Set(i, t)
+ requires 0 <= (i && (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]))
+}
+----------
diff --git a/Test/jennisys0/ExtensibleArray.jen b/Test/jennisys0/ExtensibleArray.jen new file mode 100644 index 00000000..8a6b7a6d --- /dev/null +++ b/Test/jennisys0/ExtensibleArray.jen @@ -0,0 +1,47 @@ +class ExtensibleArray[T] {
+ var Contents: seq[T]
+
+ constructor Init()
+ {
+ Contents := []
+ }
+
+ method Get(i) returns (t)
+ requires (0 <= i) && i < |Contents|
+ {
+ t := Contents[i]
+ }
+
+ method Set(i, t)
+ requires (0 <= i) && 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])
+}
diff --git a/Test/jennisys0/Prog0.jen b/Test/jennisys0/Prog0.jen new file mode 100644 index 00000000..cd847846 --- /dev/null +++ b/Test/jennisys0/Prog0.jen @@ -0,0 +1,34 @@ +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 true
+ 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 {
+}
diff --git a/Test/jennisys0/runtest.bat b/Test/jennisys0/runtest.bat new file mode 100644 index 00000000..419c8891 --- /dev/null +++ b/Test/jennisys0/runtest.bat @@ -0,0 +1,10 @@ +@echo off
+setlocal
+
+set JENNISYS_EXE=..\..\Jennisys\Jennisys\bin\Debug\Jennisys.exe
+
+for %%f in (Prog0.jen ExtensibleArray.jen) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %JENNISYS_EXE% %* /trace %%f
+)
|