Proof in flat specifications

MaRDI QIDQ4702600zbMATH OpenFDO

Authors Peter Padawitz

Publication date 1 April 2001

zbMATH Keywords

correctnessdata typesprototypingverification methods

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65)

Review text

This paper deals with the verification of data types. Especially are concidered a uniform syntax for constructor-based specifications of visible and hidden data types, Gentzen clauses, rules and proofs as a uniform schema, a simple model- and proof-theoretical basis for correctness, syntactical criteria for the main conditions on specifications. For the entire collection see [Zbl 0973.68002].

Recommendations

• scientific article; zbMATH DE number 4128365
• scientific article; zbMATH DE number 3880082
• scientific article; zbMATH DE number 4056978
• scientific article; zbMATH DE number 3911688
• Safe Data Type Specifications

Cited in

(2)

• Swinging types=functions+relations+transition systems
• Expander2: program verification between interaction and automation

This page was built for publication: Proof in flat specifications

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