Details

Autor(en) / Beteiligte

• Caplan, Joshua E.
• Harandi, Mehdi T.
• Samadzadeh, Mansur
• Zand, Mansour

Titel

A logical framework for software proof reuse

Ist Teil von

• Proceedings of the 1995 Symposium on Software reusability, 1995, p.106-113

Ort / Verlag

New York, NY, USA: ACM

Erscheinungsjahr

1995

Quelle

ACM Digital Library

Beschreibungen/Notizen

• We describe a logical framework PR for verification of reusable software components. Within our system, developers can employ the advantages traditionally associated with software reuse to reduce the cost of software verification by reusing abstract proofs and specifications. One can construct an algorithm with parameters, a specification with parameters, and a proof that the algorithm satisfies the specification provided the parameters satisfy certain conditions. Proofs in PRwill themselves contain parameters for subproofs concerning those conditions. In this framework, typing, type checking, and proof checking are decidable.