Topic: requirement specification by assertion

topics > computer science > programming > Group: requirement specification

debugging by usage rules
design documentation
path expression
predicate transforms
program proof via assertions
requirement specification by behaviors
run-time assertions
semantics by an abstract machine


Assertions on state changes provides a mathematical basis for requirements specification. The assertions, along with data structures and exception handling, form an abstract algebraic system equivalent to the desired program. Although difficult to define, such assertions should support automatic program generation. Assertions may include path restrictions on operation sequences. (cbb 5/80)
Subtopic: contract up

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

Subtopic: invariants up

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]

Subtopic: pre and post-conditions up

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]

Subtopic: state transitions up

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]

Subtopic: guards up

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

Subtopic: temporal logic up

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

Subtopic: algebraic specification up

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]

Subtopic: naming by secification up

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

Subtopic: examples up

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]

Subtopic: problems up

Quote: algebraic specification requires formal training in computer science; may limit its use

Related Topics up

Topic: debugging by usage rules (41 items)
Topic: design documentation (43 items)
Topic: path expression (14 items)
Topic: predicate transforms (7 items)
Topic: program proof via assertions (61 items)
Topic: requirement specification by behaviors (16 items)
Topic: run-time assertions (25 items)
Topic: semantics by an abstract machine
(38 items)

Updated barberCB 12/04
Copyright © 2002-2008 by C. Bradford Barber. All rights reserved.
Thesa is a trademark of C. Bradford Barber.