| Popis: |
To verify program specifications, rather than generic safety properties, it will be necessary to integrate verification into the process of programming. Program proving is unlike theorem proving in mathematics - mathematical conjectures may give no hint as to how they could be proved, but programs are written by programmers, who must understand informally why their programs work. The job of verification is not to explore some immense search space, but to formalize the programmer’s intuitions until any faults are revealed. This requires specifications and proofs that are succinct and intelligible - which in turn require logics that go beyond predicate calculus (the assembly language of program proving). In this talk, I will recount and illustrate several steps, old and new, towards this goal — particularly in the treatment of arrays. When describing arrays, program specifications are typically full of inequalities and set definitions using inequalities. For example, a diagram that a programmer might write, e.g., X: acedb |
