by Markus Roggenbach and Lutz Schröder
Abstract:
As the first of two methodological devices aimed at increasing the trust in the `correctness' of a specification, we develop a calculus for proving consistency of CASL specifications. It turns out to be possible to delegate large parts of the proof load to syntactical criteria by structuring consistency proofs along the given specification structure, so that only in rather few remaining focus points, actual theorem proving is required. The practical usability of the resulting calculus is demonstrated by extensive examples taken from the CASL library of basic data types.
Reference:
Markus Roggenbach and Lutz Schröder: Towards Trustworthy Specifications I: Consistency Checks, In Maura Cerioli, Gianna Reggio, eds.: Recent Trends in Algebraic Specification Techniques, 15th International Workshop, WADT 2001, Lecture Notes in Computer Science, vol. 2267, Springer; Berlin; http://www.springer.de, 2001. [preprint]
Bibtex Entry:
@InProceedings{RS01,
author = {Markus Roggenbach and Lutz Schr{\"o}der},
title = {Towards Trustworthy Specifications {I}: Consistency Checks},
year = {2001},
editor = {Maura Cerioli and Gianna Reggio},
booktitle = {Recent Trends in Algebraic Specification Techniques, 15th International Workshop, WADT 2001},
publisher = {Springer; Berlin; http://www.springer.de},
series = {Lecture Notes in Computer Science},
volume = {2267},
keywords = {CASL consistency structured specifications},
url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2267&spage=305},
comment = {<a href="http://www8.informatik.uni-erlangen.de/~schroeder/papers/consistency.ps">[preprint]</a>},
abstract = {As the first of two methodological devices aimed at increasing the trust in the `correctness' of a specification, we develop a calculus for proving consistency of CASL specifications. It turns out to be possible to delegate large parts of the proof load to syntactical criteria by structuring consistency proofs along the given specification structure, so that only in rather few remaining focus points, actual theorem proving is required. The practical usability of the resulting calculus is demonstrated by extensive examples taken from the CASL library of basic data types.
},
}