Inductive assertion method for logic pograms
Certain properties of logic programs are inexpressible in terms of their declarative semantics. One example of such properties would be the actual form of procedure calls and successes which occur during computations of a program. They are often used by programmers in their informal reasoning. In this paper, the inductive assertion method for proving partial correctness of logic programs is introduced and proved sound. The method makes it possible to formulate and prove properties which are inexpressible in terms of the declarative semantics. An execution mechanism using the Prolog computation rule and arbitrary search strategy (e.g., OR-parallelism or Prolog backtracking) is assumed. The method may also be used to specify the semantics of some extra-logical built-in procedures for which the declarative semantics is not applicable.
- A language of specified programs
- An axiomatic basis for computer programming
- Contributions to the Theory of Logic Programming
- Derivation of Logic Programs
- scientific article; zbMATH DE number 3872640 (Why is no real title available?)
- scientific article; zbMATH DE number 3924108 (Why is no real title available?)
- scientific article; zbMATH DE number 4037276 (Why is no real title available?)
- scientific article; zbMATH DE number 44976 (Why is no real title available?)
- scientific article; zbMATH DE number 3302923 (Why is no real title available?)
- Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
- Relating logic programs and attribute grammars
- Some global optimizations for a PROLOG compiler
- Norms on terms and their use in proving universal termination of a logic program
- Reasoning about prolog programs: From modes through types to assertions
- A new technique for verifying and correcting logic programs
- On the verification of finite failure
- Weakest preconditions for pure Prolog programs
- scientific article; zbMATH DE number 3874578 (Why is no real title available?)
- scientific article; zbMATH DE number 4037276 (Why is no real title available?)
- Proof method of partial correctness and weak completeness for normal logic programs
- On definite program answers and least Herbrand models
- Verification of logic programs
- A simple correctness proof for magic transformation
- Logic programs as specifications in the inductive verification of logic programs
- The Prolog debugger and declarative programming
- Proving completeness of logic programs with the cut
- Correctness and completeness of logic programs
- Inductive assertions and operational semantics
- S-semantics -- an example
- Implementing backjumping by means of exception handling
This page was built for publication: Inductive assertion method for logic pograms
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1105352)
