Quote: assertions define the contract between caller and called routines [»meyeB10_1992]

Quote: class invariants apply to all routines, while pre- and post-conditions apply to individual routines

Quote: class invariants specify the conventions for borderline cases, initial states, etc.; e.g., can position a CHAIN object before the start [»meyeB9_1990]

Quote: each class and routine in an Eiffel library is formally specified with preconditions, postconditions, and invariants [»meyeB9_1990]

Quote: Eiffel assertions are boolean expressions (includes function calls); no side-effects or errors [»meyeB10_1992]

Quote: if redeclare an inherited routine, can weaken its precondition or strengthen its postcondition [»meyeB10_1992]

Quote: a precondition limits the cases that a routine must be prepared to handle; simplifies the code [»meyeB9_1990]

Quote: describe terminating programs by their effect on the state of a data structure

Quote: define modules by assertions about state information and state changes; include exception conditions [»robiL9_1975, OK]

Quote: use tables to specify the post-value of a variable for various combinations of pre-values [»parnDL12_1994]

Quote: uses accents to distinguish the value of x before and after execution [»hehnEC2_1984]

Quote: allow existential variables in specification predicates; if satisfiable then perform the right-hand-side [»bealNC_1981]

Quote: specify liveness axioms by temporal logic; uses box for henceforth and diamond for eventually; defines leads_to [»lampL1_1989]

Quote: an algebraic specification of an abstract type consists of its syntax (names, domains, ranges) and the relations of its operations [»guttJV6_1977]

Quote: algebraic specification allows multiple implementations of an abstract data type [»guttJV6_1977]

Quote: algrebraic specification should scale; at any level, its size and complexity is independent of the size and complexity of the system being described [»guttJV6_1977]

Quote: algebraic specifications are conjunctions of predicates without negation or disjunction [»hoarCA9_1987]

Quote: every program is a transition axiom specification; a compiler translates the program's explicit and implicit state functions [»lampL1_1989]

QuoteRef: guttJV12_1974 ;;54 dyadic specification by operations and axioms-- i.e. an algebraic system

Quote: the union of two commands is an abstract command that is satisfied by either component [»hoarCA8_1986]

Quote: a specification in Clear consists of declarations followed by an expression made of theory-building operations [»bursRM8_1977]

Quote: Model II specifies a program by describing the source and target data and by asserting relations between these [»prywNS10_1979]

Quote: currently, Model II specifies a relation by an equation with the target variable on the left hand side [»prywNS10_1979]

Quote: the weakest specification is 'true' which is achieved by every mechanism, while 'false' is achieved by none [»hehnEC2_1984]

Quote: a refinement's name is also its precise specification; so prove that refinement matches its name [»redeDH7_1979]

Quote: algebraic specification of the abstract type, Knowlist [»guttJV6_1977]

Quote: FEA was developed for semantic information retrieval; also used for program assertions and potentially for non-procedural programming [»postSW7_1978]

Quote: algebraic specification requires formal training in computer science; may limit its use [»guttJV6_1977]