Formal Specification

Summary

• Specification
• First Order Logic
• Object Constraint Language
• Sorting
• Process
  • Signature
  • Preconditions
  • Postcondition
• Permutation
  • Signature
  • Precondition
  • Postcondition

Specification

What a program is supposed to do

Could be informal, structured, or mathematical

First Order Logic

FOL is a mathematical notation

Enables you to express propositions, combine them, and quanitfy them

Object Constraint Language

OCL is a part of UML

OCL provides a syntax for FOL that can annotate UML

Sorting

Working example:

SORT function takes an input vector of integers X and returns another vector of integers Y sorted in ascending order.

Y contains all the elements of X such that for each element in Y, the next element will be greater than or equal to the current element, except for the last element

Need to specify input and output types

Be careful of circular definition

• Given is a vector of integers named X
• Produced is a vector of integers named Y
• The output vecotr Y must be ordered
• The contents of Y must be “the same as” the contents of X
  • Everything in X must be in Y
  • Everything in Y must have come from X
  • The number of occurences of each item in Y must be equal to the number of occurences in X

Process

FOL is used to avoid verbose English

Break specification into:

1. Signature
2. Precondition
3. Postcondition

Signature

The signature gives:

• ths name of the program
• the names and types of inputs
• the names and types of outputs

Vector<int> Y = SORT(Vector<int> X)

The names of variables in the signature is used for the pre and post conditions

Preconditions

Assertions about the input arguments in the signature

Postcondition

Asserts on the output of the function

Typically expressing how the output relates to the input

For impure functions, you must specify side-effects

For each element in the output vector Y, if there exists an element after the current element, then it must be greater than or equal to the current element. If there are no elements after, than the current element must be greater than or equal to all other elements.

$$\forall i : 1 \le i \le |Y| \cdot Y[i] \le Y[i+1]$$

“dot” means “must be the case”

X has the same elements as Y if the elements of X are a permutation of Y

Permutation

Signature

bool Z = PERMUTATION(Vector<int> X, Vector<int> Y)

Precondition

$$|X| = |Y|$$

Postcondition

Empty-Case

$$|X| = 0 \Rightarrow PERMUTATION(X, Y)$$

Non-empty Case

$$|X| > 0 \land X[1] = Y[1] \land PERMUTATION(\text{tail}(X), \text{tail}(Y))$$

$$\Rightarrow PERMUTATION(X, Y)$$

Non-matching case

$$\exists j : 1 < j \le |Y| \cdot X[1] = Y[j]$$

Pasting (concat) vectors

$$Y[1..j-1] \frown Y[j+1..|Y|]$$

All together

$$PERMUTATION(X,Y) \Leftrightarrow$$

$$|X| = 0 \lor$$

$$|X| = 0 \lor (|X| > 0 \Rightarrow$$

$$(X[1] = Y[1] \land PERMUTATION(\text{tail}(X), \text{tail}(Y))) \lor$$

$$(X[1] \neq Y[1] \land \exists j : 1 < j \le |Y| \cdot X[1] = Y[j] \lor$$

$$PERMUTATION(\text{tail}(X), (Y[1..j-1] \frown Y[j+1..|Y|]))))$$

OCL of ordered

context Vector::ORDERED() : Boolean
pre: true
post: self->forAll(i : Integer | i > 0
  and i < self.length
  implies self.at[i] <= self.at[i+1])