diff options
| author |  Unknown <leino@LEINO4.redmond.corp.microsoft.com> | 2011-04-05 17:03:28 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO4.redmond.corp.microsoft.com> | 2011-04-05 17:03:28 -0700 |
| commit | 2918a80203d42a51c45872dd6900eb3677d130eb (patch) | |
| tree | 253e0ad470fd6581305f88edf61f00b7a074e5f0 /Test/dafny0/Array.dfy | |
| parent | 6e93acd001f5d23c08b02c162dc2111e531f3d5d (diff) | |
Dafny: Allow field selections and array-element selection as LHSs of assignments where RHS is not just an expression
Diffstat (limited to 'Test/dafny0/Array.dfy')
| -rw-r--r-- | Test/dafny0/Array.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/Array.dfy b/Test/dafny0/Array.dfy index 048ecd7a..60854f63 100644 --- a/Test/dafny0/Array.dfy +++ b/Test/dafny0/Array.dfy @@ -37,10 +37,10 @@ class A { method O() {
var zz2 := new A[25];
assert zz2 != zz0; // holds because zz2 is newly allocated
- /****** These would be good things to be able to verify, but the current encoding is not up to the task
var o: object := zz0;
assert this != o; // holds because zz0 has a different type
- if (zz0 != null && zz1 != null && 2 <= |zz0| && |zz0| == |zz1|) {
+ /****** This would be a good thing to be able to verify, but the current encoding is not up to the task
+ if (zz0 != null && zz1 != null && 2 <= zz0.Length && zz0.Length == zz1.Length) {
o := zz1[1];
assert zz0[1] == o ==> o == null; // holds because zz0 and zz1 have different element types
}
|