diff options
| author |  rustanleino <unknown> | 2010-03-12 09:46:44 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-03-12 09:46:44 +0000 |
| commit | aba99a56453354ee10f8c6d0b1b7ed3fbfe0d1e5 (patch) | |
| tree | cd3ec7755212a2ce28e6bc913f2683e4034b9639 /Test/dafny0/Datatypes.dfy | |
| parent | 14e28e64aaae0c5620c2d2f2a3d13350b472b1e9 (diff) | |
Added wellformedness checks to method specifications
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 8492f217..2b3168b2 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -26,7 +26,7 @@ class Node { method Add(d: int, L: List<int>) returns (r: Node)
requires Repr(L);
- ensures r.Repr(#List.Cons(d, L));
+ ensures r != null && r.Repr(#List.Cons(d, L));
{
r := new Node;
r.data := d;
|