4.2 Formal

Formal program specifications use some kind of formal description language to describe the behavior of a program. Most of these formal description languages are less ambiguous than natural languages.

In the Unified Modeling Language (UML), an activity diagram can be used to graphically illustrate the logic of a program. Similarly, pseudocode is also commonly used to describe the logic of a program. For instance, our log in logic may be expressed as follows:

$\begin{algorithmic} \STATE prompt for username and password \IF{username exist... ...ul \ENDIF \ENDIF \ELSE \STATE report log in error \ENDIF \end{algorithmic}$

In an activity diagram or a piece of pseudocode, the logic of how to do something is already specified. Sometimes, this may not be the case. The specifications of a program can merely indicates the end result of the program, without any indication of how it is done.

For example, consider a program for sorting. It may be specified as follows:

let there be an input array inp[] with n elements
the output array be out[] with n elements
for each value v found in inp[],
- assume the occurance is x in inp[]
- the occurance should be x in out[]
in out[], out[i] <= out[i+1] for all i in the range of 0 to n-1

This doesn't tell us how to write a sorting program, it just specifies the outcome.