[ jmlspecs-Things to Do-2801849 ] Create abstract syntax for level 0 JML expressions

[SourceForge.net]

Things to Do item #2801849, was opened at 2009-06-05 12:27
Message generated for change (Settings changed) made by robdyer
You can respond by visiting:
https://sourceforge.net/tracker/?func=detail&atid=545306&aid=2801849&group_id=65346

Please note that this message will contain a full copy of the comment thread,
including the initial issue submission, for this request,
not just the latest update.
Category: JAJML
Group: Level 0 support
>Status: Pending
Resolution: None
Priority: 5
Private: No
Submitted By: Curtis Clifton (cclifton)
>Assigned to: Robert Dyer (robdyer)
Summary: Create abstract syntax for level 0 JML expressions

Initial Comment:
>From the JML Ref Manual:
Some of JML's extensions to Java's expression syntax (see section 11.
Predicates and Specification Expressions), but not all of them, can be used
at level 0. Note that calls to pure methods and constructors in
spec-expressions are not part of level 0, but are only found at level 1. We
describe the level 0 specification expressions below.

The result-expression (see section 11.4.1 \result).
The old-expression (see section 11.4.2 \old and \pre).
The fresh-expression (see section 11.4.9 \fresh).
The nonnullelements-expression (see section 11.4.14 \nonnullelements).
The informal-description (see section 11.4.15 Informal Predicates).
The typeof-expression (see section 11.4.16 \typeof).
The elemtype-expression (see section 11.4.17 \elemtype).
The type-expression (see section 11.4.18 \type).
The spec-quantified-expr (see section 11.4.24 Quantified Expressions) forms
that use the quantifier keywords \forall and \exists (see section 11.4.24.1
Universal and Existential Quantifiers).
(The quantifier keywords \max, \min, \product, and \sum (see section
11.4.24.2 Generalized Quantifiers), as well as \num_of (see section
11.4.24.3 Numerical Quantifier, are all level 1 features.)

The <: operator (see section 11.6.1 Subtype operator).
The <==> and <=!=> operators (see section 11.6.2 Equivalence and
Inequivalence Operators).
The ==> and <== operators (see section 11.6.3 Forward and Reverse
Implication Operators).
The syntax for store-refs (see section 11.7 Store Refs).


----------------------------------------------------------------------

You can respond by visiting:
https://sourceforge.net/tracker/?func=detail&atid=545306&aid=2801849&group_id=65346

------------------------------------------------------------------------------
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-developers mailing list
Jmlspecs-developers@...
https://lists.sourceforge.net/lists/listinfo/jmlspecs-developers