Name
Abstract | ||
|---|---|---|
We present in this paper a methodology for verifying the partial correctness of programs written in a logic programming language with modules supporting local and contextual definitions of predicates. The methodology is a generalization of the one described in [5] and [6], originally developed for ordinary logic programs. To deal with the aspects of locality and contextual dependency, we introduce specifications for predicates in modules that are parametric on the context-dependent predicates. The verification of a program then consists in showing that for all possible contexts, what is true in those contexts satisfies the specification. The inductive technique introduced in [5, 6] is also generalized for the purpose of this verification. We then extend this technique to open programs consisting of isolated modules, and propose a compositional approach to the verification of modular programs. |
Year | DOI | Venue |
|---|---|---|
1996 | 10.1007/3-540-61630-6_20 | APPIA-GULP-PRODE |
Keywords | DocType | Volume |
satisfiability,context dependent | Conference | 1126 |
ISSN | ISBN | Citations |
0302-9743 | 3-540-61630-6 | 0 |
PageRank | References | Authors |
0.34 | 15 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Vasco Pedro | 1 | 45 | 5.13 |
| Luís Monteiro | 2 | 126 | 19.98 |