Re: "\created" primitive expression for JML
|
View:
New views
12 Messages
—
Rating Filter:
Alert me
|
 |
|
|
|
Re: "\created" primitive expression for JML
by David Naumann
::
Rate this Message:
On Wed, 19 Aug 2009, Marieke Huisman wrote:
... >> While it seems possible to cook up artificial examples, it would seem >> that most practical examples of quantifiers want to work on created >> objects anyway, so we could (a) have the created field in objects and >> (b) have a default range restriction to created objects, which would >> simplify things from the proposal. I had a conversation with Peter >> Mueller about this at Dagstuhl and he seems to favor that alternative. > In that case, the description would also need a use case for \created > outside of a quantifier. > > In Dagstuhl we discussed that there was a problem with for example > Integer objects in this case: a quantification over Integer objects > would typically be over all possible integers, not only over those that > happen to be created at that point in the program. I think we realised > that for mutable objects quantification over created objects seems to be > the default behaviour, while for immutable objects quantification over > all objects would have to be the default. > > And, if the default would be to quantify over created objects only, > there should be a way to range over all objects as well. I'm doubtful about making the default be dependent on the distinction between mutable and immutable. For one thing, immutability is a subtle notion that I would prefer to see disentangled from other core features. For another thing, the distinction doesn't seem right in all cases. Qantifying over 'all Integer objects' seems to make sense if these are serving to model what is really a mathematical type (like JMLObjectSet), but otherwise methinks the created objects are often the ones of interest even if the type is deeply immutable. For example, a fresh String is one that is !equal to all created Strings. Using the Flyweight pattern, one might want to say "all created Glyphs are on display in the menu"; or "there is no created Glyph for the character". I'm not sure I understand what is meant by 'default' for quantification, or how a default of created could be overridden. If \forall o:T means all possible objects, then predicate \created(o) can be used to restrict the range. If instead \forall means created objects, do we need anti-predicates :) to expand the range? How about a simple type-independent syntax sugar: a variation on the \forall keyword, say \forallc, with desugaring \forallc o:T; P ---> \forall o:T; \created(o) ==> P ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
|
|
|
Re: "\created" primitive expression for JML
by Erik Poll
::
Rate this Message:
Hi all,
Let me begin by saying that I haven't found I needed to use quantifiers over objects very often in specs I wrote, and most (if not all) tended to be be quantifications of objects in some array or collection, where the whole issue doesn't arise - as these object have obviously all been created. I guess typically one only cares about quantifying over objects that have been created, so that having this as a default, as Peter Muller suggest to Gary, makes sense. I can see only two issues to this: 1) As Marieke pointed out, when quantifying over objects like Strings, Integers, Booleans, etc, a which are more like "values" than proper "objects", quantification over all possible objects seems more intuitive. Eg, the natural way to specify one string being a prefix of another //@ ensures \result <==> (\exists String t; s.concat(t).equals(this)); boolean isPrefix(String s) is incorrect if the quantification is only over created objects. 2) A more fundamental problem is with the values of model fields: these values "exists" but are ever really "created" anywhere. Eg consider Class A { //@ public static model SomeObject c; If we have some represents-clause saying that c is double-equals some program variable, then we now that c has been created. But if we just have some relation between c and some program variables, there might not be an actual object c on the heap that satisfies the represents-clause - so in that case c might not be created. Quantifications over all SomeObject's would then exclude the value of the model field c. A link between 1) and 2) is that in 2) the the model field will often be some immutable, value-like object, eg a JMLObjectSet or something. But I agree with David that immutability is a subtle notion so we'd prefer not to let entangle it with the semantics of other constructs. As Matthias notes, the semantics of quantification remains an issue... I don't see an easy definition for the semantics of quantifications that range over some non-cretaed objects. Best, Erik ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by Richard Bubel-2
::
Rate this Message:
Dear all,
On Aug 21, 2009, at 11:25 , Erik Poll wrote: > 1) As Marieke pointed out, when quantifying over objects like Strings, > Integers, Booleans, etc, a which are more like "values" than proper > "objects", quantification over all possible objects seems more > intuitive. > > Eg, the natural way to specify one string being a prefix of > another > > //@ ensures \result <==> (\exists String t; > s.concat(t).equals(this)); > boolean isPrefix(String s) > > is incorrect if the quantification is only over created objects. first, please excuse if my question has been answered earlier, does not add anything new or is completely of the track. Just to help my understanding of immutable or value-like objects in JML: Have value-like objects an implicit invariant that states that e.g. for each int value i there is an Integer object io such that io.intValue() == i resp. that for any finite character sequence there is a String object with matching content? Because otherwise e.g. the above specification won't work even when quantifying over all (even non-existant) objects as there would exist states/interpretations in which all not yet created objects of type String might just happen to have the content 'a'. Best Regards, Richard ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by Erik Poll
::
Rate this Message:
Hi Richard,
>> 1) As Marieke pointed out, when quantifying over objects like Strings, >> Integers, Booleans, etc, a which are more like "values" than proper >> "objects", quantification over all possible objects seems more >> intuitive. >> >> Eg, the natural way to specify one string being a prefix of >> another >> >> //@ ensures \result <==> (\exists String t; >> s.concat(t).equals(this)); >> boolean isPrefix(String s) >> >> is incorrect if the quantification is only over created objects. > > first, please excuse if my question has been answered earlier, does > not add anything new or is completely of the track. Just to help my > understanding of immutable or value-like objects in JML: > > Have value-like objects an implicit invariant that states that e.g. > for each int value i there is an Integer object io such that > io.intValue() == i resp. that for any finite character sequence there > is a String object with matching content? No. My point was that one natural interpretation of the meaning of quantifications over Integer or Strings is to assume it ranges over all possible Integers and Strings. This effectively comes down to assuming this implicit invariant, and this is preceisely what is needed for the specification above to work. In my Platonic view of the world, all Strings do really exist, regardless of whether they happen to be allocated on some Java VM heap somewhere :-) Cheers, Erik ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by Gary T. Leavens-2
::
Rate this Message:
Hi Richard, Erik, David, Marieke, and all,
I agree that it's definitely more expressive to have JML's quantifiers by default range over all possible objects instead of just the created ones, and to have a way to talk about which ones are created. The only vexing question then is what does a possible object mean (e.g., does it have to satisfy the invariant?)? So I tend to agree that we should just make the quantifiers range over all possible objects (and answer the semantic questions that arise from that), and add the \created primitive. I also tend to think that the resulting expressions are clearer for human readers, as I think that (\forall Stack s; \created(s); s.size >= 0) Makes it immediately clear that the stacks "s" in the expression have been created by a program than would be the case if we made that the default in JML, in which case one would only see: (\forall Stack s; s.size >= 0) Other comments? Gary T. Leavens 439C Harris Center (Bldg. 116) School of EECS, University of Central Florida 4000 Central Florida Blvd., Orlando, FL 32816-2362 USA http://www.eecs.ucf.edu/~leavens phone: +1-407-823-4758 leavens@... -----Original Message----- From: Richard Bubel [mailto:bubel@...] Sent: Friday, August 21, 2009 7:50 AM To: jmlspecs-interest@... Subject: Re: [Jmlspecs-interest] "\created" primitive expression for JML Dear all, On Aug 21, 2009, at 11:25 , Erik Poll wrote: > 1) As Marieke pointed out, when quantifying over objects like Strings, > Integers, Booleans, etc, a which are more like "values" than proper > "objects", quantification over all possible objects seems more > intuitive. > > Eg, the natural way to specify one string being a prefix of > another > > //@ ensures \result <==> (\exists String t; > s.concat(t).equals(this)); > boolean isPrefix(String s) > > is incorrect if the quantification is only over created objects. first, please excuse if my question has been answered earlier, does not add anything new or is completely of the track. Just to help my understanding of immutable or value-like objects in JML: Have value-like objects an implicit invariant that states that e.g. for each int value i there is an Integer object io such that io.intValue() == i resp. that for any finite character sequence there is a String object with matching content? Because otherwise e.g. the above specification won't work even when quantifying over all (even non-existant) objects as there would exist states/interpretations in which all not yet created objects of type String might just happen to have the content 'a'. Best Regards, Richard ---------------------------------------------------------------------------- -- Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by Daniel M. Zimmerman-2
::
Rate this Message:
--On 21 August 2009 09:30:33 -0400 "Gary T. Leavens" <leavens@...>
wrote: > Hi Richard, Erik, David, Marieke, and all, > > I agree that it's definitely more expressive to have JML's quantifiers by > default range over all possible objects instead of just the created ones, > and to have a way to talk about which ones are created. The only vexing > question then is what does a possible object mean (e.g., does it have to > satisfy the invariant?)? I'd think it should have to satisfy the invariant... the purpose of an invariant (it seems to me) is to specify what the possible objects are, even though it certainly is possible to subvert the constructors/factories in various ways to create objects that don't satisfy it. I'm guessing it's safe to say that when somebody writes a quantifier, they are assuming that the objects being quantified over satisfy their invariants. Not that that helps too much in terms of the semantic questions, as many classes don't have (restrictive) invariants, but it's a place to start at least. -Dan ------------------------------------------------------------------ Daniel M. Zimmerman Assistant Professor 1900 Commerce St. Box 358426 Institute of Technology, UWT Tacoma, WA 98402 dmz@... ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by David Naumann
::
Rate this Message:
On Fri, 21 Aug 2009, Erik Poll wrote:
... > In my Platonic view of the world, all Strings do really exist, > regardless of whether they happen to be allocated on some Java VM > heap somewhere :-) My understanding is that's the view of the JML documentation, as explained by oracle Leavens. One approach to semantics of forall is to consider the heap to be an infinite ref-indexed array, maintaining the invariant that boolean ghost field 'created' (usually named 'alloc') is false for all but finitely many. That's used in Boogie/Spec# for example. In fact in the work I've seen, that invariant isn't explicitly maintained, because in axiomatic semantics of 'new' one simply assumes there are fresh references available. In the model I described at Dagstuhl, the heap is a set of allocated references and a map from that set to the object states. Platonically, potential objects live in potential heaps. (A potential Iterator needs a real or potential Collection:) So there's a fairly straightforward semantics, in possible worlds style, along these lines: state s satisfies (all x :: P) iff for all extensions t of s and (allocated) refs o in t, t satisfies P[o/x] For t to be an extension means it contains all of s untouched, and is well formed (type-correct and no dangling refs). I paused for a moment worrying about Kripke semantics, but methinks this and the Boogie model get used in such a way that they're isomorphic. We are not using possible worlds to interpret implication. ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by Mattias Ulbrich
::
Rate this Message:
Hi!
2009/8/21 David Naumann <naumann@...>: > So there's a fairly straightforward > semantics, in possible worlds style, along these lines: > > state s satisfies (all x :: P) > iff > for all extensions t of s and (allocated) refs o in t, t satisfies P[o/x] > > For t to be an extension means it contains all of s untouched, and is well > formed (type-correct and no dangling refs). I paused for a moment > worrying about Kripke semantics, but methinks this and the Boogie model > get used in such a way that they're isomorphic. We are not using possible > worlds to interpret implication. This is a nice way of formulating the idea. I wonder, however, whether the heap extensions could establish the invariants of their created objects (which, I assume, would be the desired semantics). The problem is that invariants may make use of quantifiers themselves, leading to not well-founded definitions. Consider class IntTest { //@ ghost \bigint value; //@ invariant (\exists IntTest it; it.value > value); } Evaluating the invariant for the first instance of IntTest would require to check the invariant in an extended state, which, again, would require to check it in an extension of that state, ... an infinite chain of states would have to be evaluated to check the invariant. Does it hold? Does it hold when replacing "\bigint" by "int"? I reckon therefore we can probably *not* assume that the elements of the extension of the heap over which we quantify have their invariants fulfilled. That would be strange also. Greetings, Mattias -- Mattias Ulbrich Logik und Formale Methoden (Prof. Dr. P.H. Schmitt) Institut für Theoretische Informatik lfm.iti.uka.de Universität Karlsruhe ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by David Naumann
::
Rate this Message:
On Sat, 22 Aug 2009, Mattias Ulbrich wrote:
> 2009/8/21 David Naumann <naumann@...>: >> So there's a fairly straightforward >> semantics, in possible worlds style, along these lines: >> >> state s satisfies (all x :: P) >> iff >> for all extensions t of s and (allocated) refs o in t, t satisfies P[o/x] >> >> For t to be an extension means it contains all of s untouched, and is well >> formed (type-correct and no dangling refs). I paused for a moment >> worrying about Kripke semantics, but methinks this and the Boogie model >> get used in such a way that they're isomorphic. We are not using possible >> worlds to interpret implication. > > This is a nice way of formulating the idea. I wonder, however, whether the heap > extensions could establish the invariants of their created objects > (which, I assume, > would be the desired semantics). The problem is that invariants may make use > of quantifiers themselves, leading to not well-founded definitions. > > Consider > class IntTest { > //@ ghost \bigint value; > //@ invariant (\exists IntTest it; it.value > value); > } > > Evaluating the invariant for the first instance of IntTest would > require to check the > invariant in an extended state, which, again, would require to check it in an > extension of that state, ... an infinite chain of states would have to > be evaluated to > check the invariant. > > Does it hold? Does it hold when replacing "\bigint" by "int"? > > I reckon therefore we can probably *not* assume that the elements of > the extension > of the heap over which we quantify have their invariants fulfilled. > That would be strange > also. Thanks, that's a very nice example! For purposes of formalizing a semantics, dependency on an infinite number of entities does not seem to be a show-stopper, although it might be a bit too fun for RAC. I agree we should seek a notion in which invariants hold (keeping in mind that there are many unsettled issues about invariantst). Your example seems to refute my claim that the two semantics are isomorphic. The first one I described treats the heap as an array indexed by the infinite set of references together with fields including one called 'alloc'. In an infinite heap it's quite possible that every instance of IntSet satisfies its invariant - provided there are infinitely many instances. Here's a variation on the invariant this.\alloc ==> (\exists IntTest it; it.value > value && it.\alloc) If one IntSet is allocated, and all instances satisfy the invariant, then there must be infinitely many allocated. Perhaps this is compatible with the axiomatizatic semantics of some verifiers based on this heap model. In the second semantics I described, I intend to model only the allocated objects so the heap is finite and the only way for all instances of IntTest to satisfy their invariant is for there to be no instances. One lesson of the example is that an invariant can be unsatisfiable for nonobvious reasons concerning the language semantics. In several published methodologies for invariants there are restrictions on the declarations of object invariants, in particular disallowing or restricting the use of quantifiers. Quantifying over allocated objects already has hazards (e.g., see Pierik, Clarke, and deBoer in FM'05). cheers, dave ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
|
|
Re: "\created" primitive expression for JML
by Jooyong Lee
::
Rate this Message:
Hi all,
I read this discussion interestingly. It looks as if there is one general consensus in the midst of the conflict of ideas: The created-objects option matches the user's need in most cases while there are critical corner cases where the all-objects option is better suited. Based on this observation, Gary's first suggestion - the one where created-objects option is used by default - could help more users than the second suggestion (i.e., the all-objects option) could. I wish that JML would provide two levels of quantifiers: one for regular Java developers who are likely to reason with the Java model in most cases, and the other one for more-abstract-level-specification writers who tend to reason with mathematical model. I guess this distinction of quantifiers can be made with the "allocated" field David explained. Regards, Jooyong On Sat, Aug 22, 2009 at 11:34 AM, David Naumann<naumann@...> wrote: > On Sat, 22 Aug 2009, Mattias Ulbrich wrote: >> 2009/8/21 David Naumann <naumann@...>: >>> So there's a fairly straightforward >>> semantics, in possible worlds style, along these lines: >>> >>> state s satisfies (all x :: P) >>> iff >>> for all extensions t of s and (allocated) refs o in t, t satisfies P[o/x] >>> >>> For t to be an extension means it contains all of s untouched, and is well >>> formed (type-correct and no dangling refs). I paused for a moment >>> worrying about Kripke semantics, but methinks this and the Boogie model >>> get used in such a way that they're isomorphic. We are not using possible >>> worlds to interpret implication. >> >> This is a nice way of formulating the idea. I wonder, however, whether the heap >> extensions could establish the invariants of their created objects >> (which, I assume, >> would be the desired semantics). The problem is that invariants may make use >> of quantifiers themselves, leading to not well-founded definitions. >> >> Consider >> class IntTest { >> //@ ghost \bigint value; >> //@ invariant (\exists IntTest it; it.value > value); >> } >> >> Evaluating the invariant for the first instance of IntTest would >> require to check the >> invariant in an extended state, which, again, would require to check it in an >> extension of that state, ... an infinite chain of states would have to >> be evaluated to >> check the invariant. >> >> Does it hold? Does it hold when replacing "\bigint" by "int"? >> >> I reckon therefore we can probably *not* assume that the elements of >> the extension >> of the heap over which we quantify have their invariants fulfilled. >> That would be strange >> also. > > Thanks, that's a very nice example! For purposes of formalizing a > semantics, dependency on an infinite number of entities does not seem to > be a show-stopper, although it might be a bit too fun for RAC. I agree we > should seek a notion in which invariants hold (keeping in mind that there > are many unsettled issues about invariantst). > > Your example seems to refute my claim that the two semantics are > isomorphic. The first one I described treats the heap as an array indexed > by the infinite set of references together with fields including one > called 'alloc'. In an infinite heap it's quite possible that every > instance of IntSet satisfies its invariant - provided there are infinitely > many instances. > > Here's a variation on the invariant > this.\alloc ==> (\exists IntTest it; it.value > value && it.\alloc) > > If one IntSet is allocated, and all instances satisfy the invariant, then > there must be infinitely many allocated. Perhaps this is compatible with > the axiomatizatic semantics of some verifiers based on this heap model. > > In the second semantics I described, I intend to model only the allocated > objects so the heap is finite and the only way for all instances of > IntTest to satisfy their invariant is for there to be no instances. One > lesson of the example is that an invariant can be unsatisfiable for > nonobvious reasons concerning the language semantics. > > In several published methodologies for invariants there are restrictions > on the declarations of object invariants, in particular disallowing or > restricting the use of quantifiers. Quantifying over allocated objects > already has hazards (e.g., see Pierik, Clarke, and deBoer in FM'05). > > cheers, dave > > > ------------------------------------------------------------------------------ > Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day > trial. Simplify your report design, integration and deployment - and focus on > what you do best, core application coding. Discover what's new with > Crystal Reports now. http://p.sf.net/sfu/bobj-july > _______________________________________________ > Jmlspecs-interest mailing list > Jmlspecs-interest@... > https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest > > ------------------------------------------------------------------------------ Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day trial. Simplify your report design, integration and deployment - and focus on what you do best, core application coding. Discover what's new with Crystal Reports now. http://p.sf.net/sfu/bobj-july _______________________________________________ Jmlspecs-interest mailing list Jmlspecs-interest@... https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest |
| Free embeddable forum powered by Nabble | Forum Help |
