Re: [Jmlspecs-developers] .jml file processing and refines clauses

[Wladimir de Lara Araujo Filho]

        Hi, all,

        I agree with the simplifications.

        I have a question regarding the semantics of the application of
modifiers and refinement. For a type X declared in X.java and X.refines-spec
in which the latter includes the appropriate refine declaration, the nullity
modifiers on a method specification must match. However, this is not the
case for purity. X.refines-spec can declare a method pure that is not
declared so in the .java file. The reverse is not allowed.

        First, is there a reason for this inconsistency? Second, if there
isn't one, would there be a problem to have nullity behave the same as
purity w.r.t. refinement?

                Cheers,

Wladimir de Lara Araujo Filho
260 Besserer St. suite 602
Ottawa-ON Canada
K1N 1J3
Phone [phone]

There are three schools of magic.
One: State a tautology, then ring the changes on its
corollaries;  that's philosophy.
Two: Record many facts. Try to find a pattern.
Then make a wrong guess at the next fact; that's science.
Three: Be aware that you live in a malevolent Universe controlled
by Murphy's Law, sometimes offset by
Brewster's Factor; that's engineering.
-- Robert A. Heinlein

> -----Original Message-----
> From: jmlspecs-developers-bounces@... [mailto:jmlspecs-
> developers-bounces@...] On Behalf Of Gary T. Leavens
> Sent: May 12, 2008 1:48 PM
> To: David Cok
> Cc: JML developers list; JML interest list
> Subject: Re: [Jmlspecs-developers] .jml file processing and refines
> clauses
>
>
> This kind of simplification is something we should seriously consider
> now, as we are redoing the basic tools.  I agree that the benefits of
> such a simplification in terms of tools and teaching are significant
> and thus I personally support such a simplication.  Would anyone's
> specifications break horribly if we adopted this simplification?
>
> > Another note: statements (e.g. loop invariants) that are embedded in the
> body
> > of a method are always found in the .java file.
>
> That's right.
>
> > Pet peeve: Since I like the .spec and .jml suffixes, I have always
> wished
> > that those suffixes preceded the .java suffix.
>
> That is, that the MRCU would be in the .spec or .jml file.
>
>          Gary T. Leavens
>          210 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: [phone]
>          leavens@...
>
> -------------------------------------------------------------------------
> This SF.net email is sponsored by: Microsoft
> Defy all challenges. Microsoft(R) Visual Studio 2008.
> http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
> _______________________________________________
> Jmlspecs-developers mailing list
> Jmlspecs-developers@...
> https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers

-------------------------------------------------------------------------
This SF.net email is sponsored by: Microsoft
Defy all challenges. Microsoft(R) Visual Studio 2008.
http://clk.atdmt.com/MRT/go/vse0120000070mrt/direct/01/
_______________________________________________
Jmlspecs-interest mailing list
Jmlspecs-interest@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-interest