diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-11 19:46:44 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-11 19:46:44 -0700 |
| commit | 4c3d68142ca387c0cac5da85a6d3710455a5efe2 (patch) | |
| tree | 8e8638f1bf2d70797a1b7dc38225dee64edac8a6 /Test/jennisys0 | |
| parent | f5e18a17e2d6025b071b018df9ce7cc5cf4a1d8e (diff) | |
Jennisys: First cut of injectivity analysis
Diffstat (limited to 'Test/jennisys0')
| -rw-r--r-- | Test/jennisys0/Answer | 7 | ||||
| -rw-r--r-- | Test/jennisys0/ExtensibleArray.jen | 3 | ||||
| -rw-r--r-- | Test/jennisys0/runtest.bat | 2 |
3 files changed, 7 insertions, 5 deletions
diff --git a/Test/jennisys0/Answer b/Test/jennisys0/Answer index 609f2fe3..5a3f9e82 100644 --- a/Test/jennisys0/Answer +++ b/Test/jennisys0/Answer @@ -1,6 +1,6 @@ -------------------- Prog0.jen --------------------
-Jennisys, Copyright (c) 2011, Microsoft.
+// Jennisys, Copyright (c) 2011, Microsoft.
---------- Given Jennisys program ----------
class C {
var a: seq[int]
@@ -48,7 +48,7 @@ code C { ----------
-------------------- ExtensibleArray.jen --------------------
-Jennisys, Copyright (c) 2011, Microsoft.
+// Jennisys, Copyright (c) 2011, Microsoft.
---------- Given Jennisys program ----------
class ExtensibleArray[T] {
var Contents: seq[T]
@@ -83,7 +83,8 @@ model ExtensibleArray[T] { 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]
+ more != null ==> (forall i :: 0 <= i && i < |more.Contents| ==> more.Contents[i] != null && more.Contents[i].Length = 256)
+ more != null ==> (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 index e6141ab7..7ef36ce2 100644 --- a/Test/jennisys0/ExtensibleArray.jen +++ b/Test/jennisys0/ExtensibleArray.jen @@ -34,6 +34,7 @@ model ExtensibleArray[T] { more != null ==> M < length
length = |Contents|
- forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256]
+ more != null ==> forall i :: 0 <= i && i < |more.Contents| ==> more.Contents[i] != null && more.Contents[i].Length = 256
+ more != null ==> 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/runtest.bat b/Test/jennisys0/runtest.bat index 419c8891..6bae956e 100644 --- a/Test/jennisys0/runtest.bat +++ b/Test/jennisys0/runtest.bat @@ -6,5 +6,5 @@ set JENNISYS_EXE=..\..\Jennisys\Jennisys\bin\Debug\Jennisys.exe for %%f in (Prog0.jen ExtensibleArray.jen) do (
echo.
echo -------------------- %%f --------------------
- %JENNISYS_EXE% %* /trace %%f
+ %JENNISYS_EXE% %* /trace /noAnalysis %%f
)
|