Writing correct recursive definitions of functions - Again

Documentation and user's manual

Table of contents

OCaml programs

Writing correct recursive definitions of functions - Again

To say a recursive definition of a functional value (assume it is named  f ) is correct has no meaning if there does not exist a specification for  f .

So, assume there exists a specification for  f . Then: Saying a recursive definition of  f  is correct means that it meets this specification.

A specification for  f  says ...

Correctness means both: Partial correctness: if an application of  f  to an argument in its specified domain terminates then its result meets the specification. Termination: any application of  f  to an argument in its specified domain produces a result, which means: No infinite looping. No run-time error.

To prove the correctness of a recursively-defined function, use induction!

Proving partial correctness is usually more difficult than proving termination. Here termination only will be considered. However there will be no proof. Rules to ensure termination are given below.

For each value  x  write  f (x)  as an expression e such that: Basis rule: If  x  is in the basis: no application of  f  in e. Induction rule: If  x  is not in the basis: any application of  f  in e has argument closer to the basis than  x .

Writing correct recursive definitions of functions - Again

Documentation and user's manual

Table of contents

OCaml programs