Portal de Periódicos da CAPES

A sharp proof rule for procedures in wp semantics

1989; Springer Science+Business Media; Volume: 26; Issue: 5 Linguagem: Inglês

10.1007/bf00289144

1432-0525

A. Bijlsma, Philip Matthews, J. G. Wiltink,

Logic, Reasoning, and Knowledge

A proof rule for the procedure call is proposed that has the property that the precondition it defines is the weakest precondition that can be inferred solely from the procedure's specification. Thus the rule enforces exactly the abstraction introduced by the specification. Gries's proof rule for the procedure call is shown not to have this property in cases when the specification involves so-called specification variables.