Formal Methods for Component Software: The Refinement Calculus Perspective. Büchi, M. & Sekerinski, E. In Weck, W., Bosch, J., & Szyperski, C., editors, Second Workshop on Component-Oriented Programming (WCOP), volume 5, of TUCS General Publication, pages 23–32, Jyväskylä, Finland, September, 1997. Turku Centre for Computer Science.
Formal Methods for Component Software: The Refinement Calculus Perspective [link]Paper  abstract   bibtex   1 download  
We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Nondeterminism in specifications permits enhancements and alternate implementations. A formally verifiable refinement relationship between specification and implementation of a component ensures compliance with the published specification. Unambiguous and complete contracts are the foundation for any component market.
@inproceedings{BuchiSekerinski97Components,
	address = {Jyväskylä, Finland},
	series = {{TUCS} {General} {Publication}},
	title = {Formal {Methods} for {Component} {Software}: {The} {Refinement} {Calculus} {Perspective}},
	volume = {5},
	url = {https://tucs.fi/publications/view/?pub_id=bWeBoSzy97},
	abstract = {We exhibit the benefits of using formal methods for constructing and documenting component software. Formal specifications provide concise and complete descriptions of black-box components and, herewith, pave the way for full encapsulation. Nondeterminism in specifications permits enhancements and alternate implementations. A formally verifiable refinement relationship between specification and implementation of a component ensures compliance with the published specification. Unambiguous and complete contracts are the foundation for any component market.},
	booktitle = {Second {Workshop} on {Component}-{Oriented} {Programming} ({WCOP})},
	publisher = {Turku Centre for Computer Science},
	author = {Büchi, Martin and Sekerinski, Emil},
	editor = {Weck, Wolfgang and Bosch, Jan and Szyperski, Clemens},
	month = sep,
	year = {1997},
	pages = {23--32},
}

Downloads: 1