Relations as executable specifications: taming partiality and non-determinism using invariants

DOI10.1007/978-3-642-33314-9_10MaRDI QIDQ2915141zbMATH OpenOpenAlexFDO

Authors Nuno Macedo, Hugo Pacheco, Alcino Cunha

Publication date 21 September 2012

Published in Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-33314-9_10

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 475192
• scientific article; zbMATH DE number 1086634
• Relations as abstract datatypes: An institution to specify relations between algebras
• Mathematics of Program Construction
• A RELATIONAL MODEL OF DEMONIC NONDETERMINISTIC PROGRAMS

Cites work

• A programmable editor for developing structured documents based on bidirectional transformations
• Bidirectionalization for free! (Pearl)
• Bidirectionalization transformation based on automatic derivation of view complement functions
• Bidirectionalizing graph transformations
• Combinators for bi-directional tree transformations: a linguistic approach to the view update problem
• Combining syntactic and semantic bidirectionalization
• Extended Static Checking by Calculation Using the Pointfree Transform
• Generic point-free lenses
• Gradual refinement. Blending pattern matching with data abstraction
• scientific article; zbMATH DE number 1612493 (Why is no real title available?)
• scientific article; zbMATH DE number 910715 (Why is no real title available?)
• Multi-paradigm Declarative Languages
• Programming from Galois connections
• Programming Languages and Systems
• Quotient lenses
• Relations as executable specifications: taming partiality and non-determinism using invariants
• Transformation of structure-shy programs with application to XPath queries and strategic functions

Cited in

(2)

• Relations as executable specifications: taming partiality and non-determinism using invariants
• Relaxing Restrictions on Invariant Composition in the B Method by Ownership Control a la Spec#

Describes a project that uses

Uses Software

• XPath

This page was built for publication: Relations as executable specifications: taming partiality and non-determinism using invariants

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2915141)