Advantages of Formal Methods

1. Reduces the need for debugging
2. Forces a clear formulation of program objectives
3. Makes reusing software easier
4. Commercial imperatives

The subset of our analysis are Pieces of Code - a self contained program (here written as pseudo-code), which acts as a function on its inputs. We assume this pseudo-code is made up of:

1. Usual arithmetic operators and library functions (eg $+$, $*$, etc)
2. if-then and if-then-else constructs
3. The while construct

Note:

• No type declarations (use context)
• No input/output statements