A Logic for Correct Program Development

摘要: Existing verification technology, though theoretically adequate, is not directly applicable to the construction of large software systems. This thesis explores view that reasoning about code proper paradigm for correct program development. Instead, specifications should be objects study and a logic formulated constructively proving have acceptable implementations; from these proofs may extracted. Thus, constructive existence become programmer''s main concern, while executable text seen as valuable by-product which cannot produced incorrect reasoning. The captures this development in formal refinement specifications. Specifications are written an imperative notation generalized assignment; they allow calculations integer arithmetic finite set theory. Classical techniques shown inconsistent domain (where propositions claim programs), hence alternative developed based on intuitionistic Proofs trees, stylistically similar those Gerhard Gentzen''s sequent calculus. It argued linear appropriate when presented paper, hierarchical with machine aid. A mechanism described extracts codes valid proofs; its assures consistency logic. Finally, several optimization examined applied extracted sample proofs. concludes discussion expounded development, suggestions system view, look at numerous research problems remaining area.