diff options
| author |  Unknown <t-alekm@A3479878.redmond.corp.microsoft.com> | 2011-07-26 14:50:28 -0700 |
|---|---|---|
| committer | Unknown <t-alekm@A3479878.redmond.corp.microsoft.com> | 2011-07-26 14:50:28 -0700 |
| commit | c559018a94ea1f6fbc552aecc05e37a90ea39111 (patch) | |
| tree | 9f9c1f12c12dde0d5f8aa15dd399f6a6cb8e1fa7 /Jennisys/examples | |
| parent | a45797859355d29f791cdbe7d498f1b15938bc27 (diff) | |
Jennisys:
- added "inferConds" cmd line option
- refactored out some pieces of code into their own functions
Diffstat (limited to 'Jennisys/examples')
| -rw-r--r-- | Jennisys/examples/List2.jen | 2 | ||||
| -rw-r--r-- | Jennisys/examples/List3.jen | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/Jennisys/examples/List2.jen b/Jennisys/examples/List2.jen index 61fad148..116804fa 100644 --- a/Jennisys/examples/List2.jen +++ b/Jennisys/examples/List2.jen @@ -8,7 +8,7 @@ class IntList { ensures list = [2] constructor OneTwo() - ensures list = [1] + [2] + ensures list = [1 2] constructor Singleton(p: int) ensures list = [p] diff --git a/Jennisys/examples/List3.jen b/Jennisys/examples/List3.jen index 776bd43d..d01300bb 100644 --- a/Jennisys/examples/List3.jen +++ b/Jennisys/examples/List3.jen @@ -8,7 +8,7 @@ class IntList { ensures list = [2] constructor OneTwo() - ensures list = [1] + [2] + ensures list = [1 2] constructor Singleton(p: int) ensures list = [p] |