Specification of Generic APIs, or Why Algebraic May Be Better than Pre/Post
Citation:
Anya Helene Bagge and Magne Haveraaen. Specification of Generic APIs, or Why Algebraic May Be Better than Pre/Post. In Tucker Taft, editor(s), Proceedings of the International Conference on High Integrity Language Technology (HILT'14). ACM, 2014.Conference:
International Conference on High Integrity Language Technology (HILT'14), Portland, Oregon, 2014, proceedings pp.Paper Links:
[doi] [pdf (final preprint)]Abstract:
Specification based on Floyd-Hoare logic, using pre and postconditions, is common in languages aimed at high integrity software. Such pre/postcondition specifications are geared towards verification of code. While this specification technique has proven quite successful in the past 40 years, it has limitations when applied to API specification, particularly specification of generic interfaces.
API-oriented design and genericity is of particular importance in modern large-scale software development. In this situation, algebraic specification techniques have a significant advantage. Unlike pre/post-based specification, which deals with the inputs and outputs of one operation at a time, algebraic specification deals with the relationships between the different operations in an API, which is needed in the specification of generic APIs.
Related Project:
Axiom TestingBibTeX:
@InProceedings{bagge-haveraaen-hilt14-apispec, title = {Specification of Generic APIs, or Why Algebraic May Be Better than Pre/Post}, author = {Bagge, Anya Helene and Haveraaen, Magne}, year = {2014}, booktitle = {Proceedings of the International Conference on High Integrity Language Technology (HILT'14)}, editor = {Tucker Taft}, publisher = {ACM}, address = {New York, NY, USA}, doi = {10.1145/2663171.2663183}, isbn = {978-1-4503-3217-0}, location = {Portland, Oregon}, url = {http://www.ii.uib.no/~anya/papers/bagge-haveraaen-hilt14-apispec.html}, pdf = {http://www.ii.uib.no/~anya/papers/bagge-haveraaen-hilt14-apispec.pdf}, }