|
|||||
|
|
Weakest preconditions for progress |
|
| Authors: | Johan J Lukkien Jan L A van de Snepscheut |
| Affiliation: | (1) Computer Science, California Institute of Technology, 91125 Pasadena, CA, USA;(2) Present address: Department of Mathematics and Computer Science, Eindhoven Technical University, P.O. Box 513, 5600 MB Eindhoven, The Netherlands |
| Abstract: | Predicate transformers that map the postcondition and all intermediate conditions of a command to a precondition are introduced. They can be used to specify certain progress properties of sequential programs. |
| Keywords: | Weakest preconditions Progress properties |
| 本文献已被 SpringerLink 等数据库收录！ | |