Part 1

Writing Specifications

Formal specifications should be concise, unambiguous, non-redundant, and expressed precisely in a formal notation. Precise language of mathematics is the preferred tool for mathematical modeling of various systems.

RESOLVE uses mathematical modeling to specify various data structures and their behavior. For example, it uses a mathematical string to model the linear structure of a stack, and a number of mathematical string operators (concatenation, substring, length, etc.) to describe it's behaviour. RESOLVE also includes a number of specification mechanisms. One of them is specification of all the operations.

The three operation specification components are:

1. operation signature that specifies names, types, and parameter modes for all the formal operation parameters.

2. requires clause - a precondition that should be true before an operation is called.

3. ensures clause - post-condition that will hold after the operation executes.