Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
From MaRDI portal
The authors define attribute grammars and show that they can be used to give an operational semantics to recursive program schemes. They define a notion of partial correctness of an attribute grammar with respect to a specification and give an inductive method for proving partial correctness. They show how this can be applied to prove correctness of imperative, applicative or logic programs. The paper is clear and includes numerous examples.
Recommendations
Cites work
- A New Incompleteness Result for Hoare's System
- An order-algebraic definition of knuthian semantics
- Attribute Grammars and Mathematical Semantics
- Attribute grammars and recursive program schemes. I. II
- Contributions to the Theory of Logic Programming
- Correctness proofs of syntax-directed processing descriptions by attributes
- Error diagnosis in logic programming an adaptation of E.Y. Shapiro's method
- Extended Attribute Grammars
- scientific article; zbMATH DE number 3972168 (Why is no real title available?)
- scientific article; zbMATH DE number 3513288 (Why is no real title available?)
- scientific article; zbMATH DE number 3550181 (Why is no real title available?)
- Initial Algebra Semantics and Continuous Algebras
- IO-macrolanguages and attributed translations
- Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II
- On the completeness of the inductive assertion method
- Relating logic programs and attribute grammars
- Simple multi-visit attribute grammars
- Speeding up circularity tests for attribute grammars
- The formal power of one-visit attribute grammars
- Theory of program structures: Schemes, semantics, verification
Cited in
(14)- Equivalences and transformations of regular systems - applications to recursive program schemes and grammars
- Inductive assertion method for logic pograms
- Context-free hypergraph grammars have the same term-generating power as attribute grammars
- Attributed tree grammars
- Attribute grammars as record calculus. -- A structure-oriented denotational semantics of attribute grammars by using Cardelli's record calculus
- Fred: An approach to generating real, correct, reusable programs from proofs
- Attribute Grammars and Categorical Semantics
- Formalising and Verifying Reference Attribute Grammars in Coq
- scientific article; zbMATH DE number 4005583 (Why is no real title available?)
- scientific article; zbMATH DE number 4090774 (Why is no real title available?)
- Can we transform logic programs into attribute grammars ?
- scientific article; zbMATH DE number 870438 (Why is no real title available?)
- Proof methods of declarative properties of definite programs
- Computational and attribute models of formal languages
This page was built for publication: Proofs of partial correctness for attribute grammars with applications to recursive procedures and logic programming
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2640347)
