Some definitions:
query - basic and derived
command
Six Principles:
- Separate queries from commands
- Separate basic queries from derived queries
-
For each derived query, write a postcondition that
specifies what result will be returned in terms of one or
more basic queries
-
For each command, write a postcondition that specifies
the value of every basic query
-
For every query and command, decide on a suitable precondition
-
Write invariants to define unchanging properties of objects
Some javadoc additions (supported by tools, but useful
without them)
-
@pre
a.k.a @require
-
@post
a.k.a @ensure
@result
@nochange
-
@invariant
-
forall
-
implies
-
exists


