diff options
| author |  rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-06 23:54:22 +0000 |
| commit | 2efa59dea051803bc716d02070aa013397cfccc4 (patch) | |
| tree | bea0fe3564ee6b336db622f8c24a13552f68d10d /Test/dafny0/Simple.dfy | |
| parent | 61993a0cf682448770a0e3223ba560171635c3af (diff) | |
Added a sequence update expression in Dafny.
Diffstat (limited to 'Test/dafny0/Simple.dfy')
| -rw-r--r-- | Test/dafny0/Simple.dfy | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index 9f89543c..5f0bee87 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -24,6 +24,7 @@ class MyClass<T,U> { var to: MyClass<T,U>;
call to, u, v := this.M(true, lotsaObjects);
call to, u, v := to.M(true, lotsaObjects);
+ assert v[x] != null ==> null !in v[2..x][1..][5 := v[this.x]][..10];
}
}
}
|