2. Semantics

Semantics

General

Foundamentals

• requires precondition-1 && precondition-2;
• ensures postcontition-1 && postcondition-2;
• signals (Exception e) (* this is true only if exception occurs*);
• assignable param; it says that param is modifiable
• assignable \nothing; means that the method doesn’t have side-effects

JML’s extension to Java expressions

• \old(E) value of E in pre-state (before the execturion of the method)
• \result result of method call
• a ⇒ b a implies b
• a ⇐ b a follows from b (i.e., b implies a)
• a ⇔ b if and only if b
• a <=!=> b not (a if and only if b)

Quantifiers

Universal quantifier

• (\forall variable; range; condition) condition must always be true

Existential quantifier

• (\exists variable; range; condition) it’s like Java’s logic operator ( ? : )

Generalized quantifiers

• (\max variable; range; operation/condition)
• (\min variable; range; operation/condition)
• (\product variable; range; operation/condition)
• (\sum variable; range; operation/condition)

Numeric quantifier

• (\num_of int i; P(i); Q(i)) cardinality of i for which P and Q are true

General outline of JML specification