BU352 Study Guide - Final Guide: Postcondition, Precondition, First-Order Logic
Document Summary
Formal veri cation is when you state a speci cation and prove a program satis es the speci cation for all inputs. We formally specify and verify programs to : reduce bugs, to test safety critical software or important components, to document individual component, to adopt a better development and veri cation process . Note : only part 3 is covered in cs245. Our assertions about programs will have the form: (p) - precondition, c - program or code, (q) - postcondition. The meaning of the triple (p) c (q) is : if program c is run starting in a state that satis es p, then the resulting state after execution of c will satisfy q. An assertion (p) c (q) is called a hoare triple. A speci cation of a program c is a hoare triple with c as the second component. A triple (p) c (q) is satis ed under partial correctness, denoted.
