ACE Take-Away: Lect No.1 Correctness

Take-Away Notes for Module COMP2048.

Termination, Partial Correctness and Total Correctness.

Definition

For every legal input , the algorithm halts / terminates when it runs on .

For every legal input , if the algorithm terminates when it runs on , then the specified relationship holds between and the resulting output set.

aka.

If the algorithm terminates(but not guaranteed to terminate), it produces the desired output.

For every legal input , the algorithm indeed terminates and the specified relationship holds between and the resulting output set.

aka.

The algorithm is guaranteed to terminate and it produces the desired output for all legal inputs.

: the set of all the legal input;

: the algorithm terminates when it runs on ;

: the specified relationship holds between and the output;

TBC. Please refer to the slides (Page 18-22) for more information.