Incorrect contracts involving derived array splices (C# format)

[mernst]

Originally reported on Google Code with ID 44

Project Member Reported by fmc3@cs.washington.edu, Feb 21, 2014

After running the daikon/test/daikon-tests for the csharp format, I observed a number
of incorrect contracts involving derived array splices. 

Here are two contracts generated for the QueueAr test:

Contract.ForAll(0, this.theArray.Slice(orig(this.front)+1, this.theArray.Count()-1).Count(),
i => this.theArray.Slice(orig(this.front)+1, this.theArray.Count()-1)[i].Equals(this.theArray.Slice(orig(this.front)+1,
Contract.OldValue(this.theArray).Count()-1)[i]))

Contract.ForAll(0, this.theArray.Slice(0, orig(this.front)-1).Count(), i => this.theArray.Slice(0,
orig(this.front)-1)[i].Equals(this.theArray.Slice(0, orig(this.front)-1)[i]))

These contracts get generated by the file derive/binary/SequenceSubsequence.java in
this code:

public String csharp_name(String index) {
    String lower = get_lower_bound().csharp_name();
    String upper = get_upper_bound().csharp_name();
    return seqvar().csharp_name() + ".Slice(" + lower + ", " + upper + ")";
}

A few observations:
1) Somewhere 'orig(..)' is not being properly translated to 'Contract.OldValue(..)'.
I tried rewriting the code similar to what JML does, but did not have success.
2) The Slice method is not currently part of CSharpDaikonLib.
3) I have never seen contracts of this format before. Perhaps we have never turned
on this derived variable?
4) There could potentially be other bugs in derived variables we have not tested

I attached the diff file were I observed these contracts. There are many other examples
of it inside the file.
    QueueAr.txt-csharpcontract.diff 
29.6 KB   Download  


Mar 16, 2014 Delete comment Project Member #1 fmc3@cs.washington.edu

I changed this to output an unimplemented message.

Reported by markro@cs.washington.edu on 2015-05-04 15:32:18

---

- _Attachment: [QueueAr.txt-csharpcontract.diff](https://storage.googleapis.com/google-code-attachments/daikon/issue-44/comment-0/QueueAr.txt-csharpcontract.diff)_

[mernst]

Reported by markro@cs.washington.edu on 2015-05-04 15:34:23