Back to University of Twente portal
Weakest Preconditions for High-Level Programs
Habel, A. and Pennemann, K.-H. and Rensink, A. (2006) Weakest Preconditions for High-Level Programs. [Report]
![[img]](http://doc.utwente.nl/style/images/fileicons/application_pdf.png)
| PDF 694Kb |
| Abstract: | In proof theory, a standard method for showing the correctness of a program w.r.t. given pre- and postconditions is to construct a weakest precondition and to show that the precondition implies the weakest precondition. In this paper, graph programs in the sense of Habel and Plump 2001 are extended to programs over high-level rules with application conditions, a formal definition of weakest preconditions for high-level programs in the sense of Dijkstra 1975 is given, and a construction of weakest preconditions is presented. |
| Item Type: | Report |
| Faculty: | Electrical Engineering, Mathematics and Computer Science (EEMCS) |
| Research Group: | |
| Link to this item: | http://purl.utwente.nl/publications/66189 |
| Official URL: | http://formale-sprachen.informatik.uni-oldenburg.de/~skript/fs-pub/hpr-techreport.pdf |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page
Metis ID: 238075