A collection of methods for the algebraic proofing of a computer program to ensure that it will satisfy some mathematical condition. To proof a program using formal methods an algebraic condition is chosen using a special mathematical language (such languages include Z and VDM) and, through a process of proofs, a pseudocode fragment is arrived at that the programmer is certain will satisfy the initial condition. This pseudocode can then be implemented using some other language such as C. Typically used by those segments of the computer industry that require safety critical coding.

Log in or registerto write something here or to contact authors.