Reaves.dev

v0.1.0

built using

Phoenix v1.7.12

Formal Specification

Stephen M. Reaves

::

2023-10-02

Notes about Lesson 7 of CS-6310

Summary

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

Process

FOL is used to avoid verbose English

Break specification into:

  1. Signature
  2. Precondition
  3. Postcondition

Signature

The signature gives:

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.

i:1iYY[i]Y[i+1]\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|X| = |Y|

Postcondition

Empty-Case

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

Non-empty Case

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

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

Non-matching case

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

Pasting (concat) vectors

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

All together

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

X=0|X| = 0 \lor

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

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

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

PERMUTATION(tail(X),(Y[1..j1]Y[j+1..Y]))))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])