Name
Abstract | ||
|---|---|---|
Summary. A proof rule for the procedure call is proposed that has the proper- ty 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. |
Year | DOI | Venue |
|---|---|---|
1989 | 10.1007/BF00289144 | Acta Inf. |
Keywords | Field | DocType |
Information System,Operating System,Data Structure,Communication Network,Information Theory | Predicate transformer semantics,Information theory,Data structure,Programming language,Abstraction,Computer science,Precondition,Semantics | Journal |
Volume | Issue | ISSN |
26 | 5 | 0001-5903 |
Citations | PageRank | References |
10 | 1.22 | 4 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| A. Bijlsma | 1 | 36 | 7.02 |
| P. A. Matthews | 2 | 13 | 1.97 |
| J G Wiltink | 3 | 16 | 3.22 |