atiti
commented
11 years ago From: (GH: None) Date: Sat Dec 15 17:20:08 2007
added mailto line
This message has 0 attachment(s)
Open atiti opened 11 years ago
atiti
commented
11 years ago From: (GH: None) Date: Sat Dec 15 17:20:08 2007
added mailto line
This message has 0 attachment(s)
atiti
commented
11 years ago From: None (GH: None) Date: Tue Apr 27 14:34:16 2010
Milestone ESCJava2 2.0.9 release deleted
atiti
commented
11 years ago From: kiniry (GH: kiniry) Date: Fri Apr 30 10:42:30 2010
This ticket should be accepted when/if we decide to upgrade our invariant handling wrt universes.
{{{
!html
Reply to: noreply@sort.ucd.ie }}} {{{ Bugs item #55, was opened at 2005-04-08 12:29 You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=441&aid=55&group_id=97
Category: Object Logic Group: v2.0a8
Initial Comment: I've been playing around with ESC/Java and I'm running into problems with invariants that have been defined in an interface.
In this example:
////////////////////////////////////////////
interface B { /@ invariant isZero() | isNonZero(); @/ /@ pure @/ boolean isZero(); /@ pure @/ boolean isNonZero(); }
class A implements B { /@ ensures a == 0; @/ A() { a = 0; }
/@ also ensures \result <==> a == 0; @/ public /@ pure @/ boolean isZero() { return a == 0; }
/@ also ensures \result <==> a != 0; @/ public /@ pure @/ boolean isNonZero() { return a != 0; }
int a; }
////////////////////////////////////////////
the invariant isZero() | isNonZero() from the baseclass B is violated in A, which seems incorrect. I can work around this in a few ways:
Maybe I'm just misunderstanding things and one of these workarounds is actually the right way to go about it ;-) Do you have any idea?
Cheers,
Peter
Peter van Rossum Radboud University Nijmegen Department of Computer Science Security of Systems Group Toernooiveld 1 6525 ED Nijmegen The Netherlands
For completeness sake, here is David Cok's emailed response as well:
Peter,
Thanks for the good example (and please enter the bug report).
It is an example of a problem that I have been aware of but have not thought through all the ramifications of.
To explain a little bit, escjava does modular checking by routine. When the constructor A() is checked, the various referenced types, e.g. B, are brought in. However, escjava does not realize that the methods of B (as used in annotations) are overridden by additional specs in A. Hence the additional specs aren't used.
If the invariant is repeated in A, then the reference to isZero or isNonZero is resolved with the definitions in A, so the relevant specs are included.
The reason that A() passes if B is a class or abstract class is a little tricky - but interesting. Remember that in this case B's constructor is executed as the first step in A(). In verifying A(), escjava assumes that B() passes it's own specifications, which include the fact that the invariant in B is satisfied. The specs in B do not depend on things in A and adding additional spec-cases by overriding methods in A can't break B's invariant (those methods have to satisfy B's invariant as well). So B's invariant must still be true at the end of A's constructor, regardless of what the overriding methods in A do - the actual specs in A do not matter (though they cannot be inconsistent with the specs in B - all that the specs in B say is that either/both isZero or isNonZero is true.
So the real difference in the two cases is that interfaces do not have constructors.
Comment By: Dermot Cochran (dcochran) Date: 2007-12-15 16:16
Message: These tickets are being transferred into the Mobius Trac
Comment By: David Cok (davidcok) Date: 2006-10-23 23:55
Message: With a little more investigation, here is what I think: In actuality B's invariant is not actually necessarily satisfied at the end of A's constructor. This is because the invariant is a statement that ALL B objects satisfy the invariant in the pre-state and must again satisfy the invariant in the post-state. However, there is no way of knowing that a B object that is not an A has not changed as a result of the assignment to a, hence the warning about the invariant in the post-state.
There ought also to be a warning when A is a superclass. The reason there is not is a bug: the invariant in that case is not included as pre-state assumption or as a post-state assertion. This is because Esc/Java was designed with just fields in invariants and only pulls in invariants with relevant fields; super class invariants with just method calls do not get pulled in.
So there are still bugs in how the VC is created but in a different direction than the submitter thought or the previous comment indicated.
Comment By: David Cok (davidcok) Date: 2006-10-23 23:53
Message: With a little more investigation, here is what I think: In actuality B's invariant is not actually necessarily satisfied at the end of A's constructor. This is because the invariant is a statement that ALL B objects satisfy the invariant in the pre-state and must again satisfy the invariant in the post-state. However, there is no way of knowing that a B object that is not an A has not changed as a result of the assignment to a, hence the warning about the invariant in the post-state.
There ought also to be a warning when A is a superclass. The reason there is not is a bug: the invariant in that case is not included as pre-state assumption or as a post-state assertion. This is because Esc/Java was designed with just fields in invariants and only pulls in invariants with relevant fields; super class invariants with just method calls do not get pulled in.
So there are still bugs in how the VC is created but in a different direction than the submitter thought or the previous comment indicated.
Comment By: Joseph Kiniry (jkiniry) Date: 2005-10-24 10:35
Message: This is an interesting little bug that is going to require some careful thinking. I'd like to assign it to Alan but make sure to talk about it with Robin and Radu so that they are kept in the loop about it and help you think about it. Please make sure to add test code for the situation and writeup the subtleties in the "Object Logic..." and "Implementation..." books.
You can respond by visiting: http://sort.ucd.ie/tracker/?func=detail&atid=441&aid=55&group_id=97 }}}