Introduction to�Formal Specifications

Prof. Indraneel Mukhopadhyay, PhD

What is Formal Specifications ?

• Specifying the functional characteristics of a software product is most important during the Analysis phase.

​

• Keep in mind it might not be applicable in all scenarios.

​

• Relational Notations : Entities & Attributes
• recurrence relations, axioms, regular expression

​

• State Oriented Notations : Functional Characteristics
• decision tables, transition tables, finite state machines

What is Formal Specifications ?

A formal software specification is a statement expressed in a language whose vocabulary, syntax, and semantics are formally defined. The need for a formal semantic definition means that the specification languages cannot be based on natural language; it must be based on mathematics.

Formal Specification

?

?

?

Pros and Cons

• Provides insights and understanding of the software requirements and design.
• Possible to prove that a program conforms to its specifications.
• Automatically Software tools

PROS

• Software management is conservative and unwilling to adopt new techniques
• Some systems are difficult to specify using existing specification techniques.

CONS

Relational Notations

• Relational notations are used based on the concept of entities and attributes. Entities are elements in a system; the names are chosen to denote the nature of the elements (e.g., stacks, queues). Attributes are specified by applying functions and relations to the named entities. Attributes specify permitted operations on entities, relationships among entities, and data flow between entities.

Relational Notations

• Relational notations include implicit equations, recurrence relations, and algebraic axioms.

State Oriented Notations

• State-oriented specifications use the current state of the system and the current stimuli presented to the system to show the next state of the system. The execution history by which the current state was attained does not influence the next state; it is dependent only on the current state and the current stimuli.

State-Oriented Notations

• State-oriented notations include decision tables, event tables, transition tables, and finite-state tables.

Specification Principles

• Principle 1: Separate functionality from implementation.

​

• A specification is a statement of what is desired, not how it is to be realized. Specifications can take two general forms. The first form is that of mathematical functions: Given some set of inputs, produce a particular set of outputs. The general form of such specifications is find [a/the/all] result such that P(input), where P

Specification Principles

• represents an arbitrary predicate. In such specifications, the result to be obtained has been entirely expressed in a “what”, rather than a “how” form, mainly because the result is a mathematical function of the input (the operation has well-defined starting and stopping points) and is unaffected by any surrounding environment.

Specification Principles

• Principle 2: A process-oriented systems specification language is sometimes required.

​

• If the environment is dynamic and its changes affect the behavior of some entity interacting with that environment (as in an embedded computer system), its behavior cannot be expressed as a mathematical function of its input. Rather a process-oriented description must be employed, in which the “what”

Specification Principles

• specification is achieved by specifying a model of the desired behavior in terms of functional responses to various stimuli from the environment.

Specification Principles

• Principle 3: The specification must provide the implementor all of the information he/she needs to complete the program, and no more.

​

• In particular, no information about the structure of the calling program should be conveyed.

Specification Principles

• Principle 4: The specification should be sufficiently formal that it can conceivably be tested for consistency, correctness, and other desirable properties.

​

• Principle 5: The specification should discuss the program in terms normally used by the user and implementor alike.

​

Some Specification Techniques

Specification Principles

• Implicit Equations

​

• Specify computation of square root of a number between 0 and some maximum value Y to a tolerance E.

​

(0<=X<=Y){ABS_VALUE[(WHAT(X)) 2-X]}<=E

Specification Principles

• Recurrence Relations

​

• Good for recursive computations. Example, Fibonacci numbers 0, 1, 1, 2, 3, 5, 8,...

FI(0) = 0, FI(1) = 1,

FI(n) = FI(n-1) + FI(n-2),n>=1.

Specification Principles

• Decision Tables

​

• Good for state-oriented specifications. Example, credit approval.

​

Specification Principles

• Event Table

​

• Specify action to be taken when events occur under different sets of conditions. f(M,E)=A, where M denotes the current set of operating conditions, E is the event of interest, and A is the action to be taken (two-dimension table).

Specification Principles

• Transition Table

​

• Used to specify changes in the state of a system as a function of driving forces. f(si,cj) = sk means if f is in state si with the condition cj then the next state is sk

Specification Principles

• Transition Table

​

• Used to specify changes in the state of a system as a function of driving forces. f(s_i,c_j) = s_k means if f is in state s_i with the condition c_j then the next state is s_k

​

• Menu-driven software systems normally are based on such tables.

Axiomatic Specification

• Use a set of stateless functions; each function has a set of pre- and post-conditions. Pre- and post-conditions are predicates over the inputs and outputs of a function. A predicate is a Boolean expression which is true or false and whose variables are the parameters of the function being specified.

Axiomatic Specification

Some predicates are:

1. A>B and C>D

2. exists i, j, k in M...N: i ² =j² + k²

3. for-all i in 1...10, exists j in 1...10: squares (i)=j ²

Axiomatic Specification

Stages of axiomatic specification of a function:

​

1. Establish the range of the input parameters over which the function is intended to behave correctly. Specify the input parameter constraints as a predicate.
2. Specify a predicate defining a condition which must hold on the output of the function if it behaves correctly.

Axiomatic Specification

3. Establish what changes (if any) are made to the function's input/output parameters. (note: in a purely mathematical function, no parameters would be changed. However, some programming languages modify parameters through call by name or call by reference.)

​

• Combine these into pre- and post-conditions for the function.

Axiomatic Specification

• Consider a search function that accepts an array of integers and some integer key of its parameters. The array members are sorted in increasing order. The function returns the array index of the member of the array whose value is equal to that of the key. The original input is unchanged. If the key is not matched, return an array index that is one number larger than the array's maximum index.

Axiomatic Specification

function Search (X: INTEGER-ARRAY; Key: INTEGER) return INTEGER;

Pre: exists i in X'FIRST...X'LAST: X(i)=Key and for-all i,j in X'FIRST...X'LAST: i<=X(j)

Post: X''(Search (X, Key))=Key and X=X‘’

Error: Search (X, Key)=X'LAST + 1

​

X'' refers to the value of the array X after the function has been evaluated.

Formal Spec. Homework Problem

Consider a function that accepts an array and then returns the greatest member of the array and the index of that member in the original array. The original input is unchanged. If the array is empty, return an array index of -1. Assume that X’FIRST and X’LAST return the indices of the first and last array members, respectively.

End of Presentation