User: Guest  Login
Title:

A Brief Study in Automating Proofs Based on a Refined Hoare-logic

Document type:
Technical Report
Author(s):
Peter Mueller; Arnd Poetzsch-Heffter
Abstract:
This report deals with program verification based on a refined Hoare-logic which allows to handle procedure calls. A certain specification technique allows to specify these procedures by pre- and postconditions. To do that, the data model of the programming language is formalized and objects of the programming language are mapped to abstract values. Specifications can thus refer to these abstract values and describe the behavior of a procedure on a higher level of abstraction. As basic operation...     »
Keywords:
verification; correctness proof; logic-based programming environments
Year:
1996
Year / month:
1996-11-01 00:00:00
Pages:
14
 BibTeX