Formal Methods for Component Software: The Refinement Calculus Perspective. Büchi, M. & Sekerinski, E. In Bosch, J. & Mitchell, S., editors, Object-Oriented Technology. ECOOP 1997, volume 1357, of Lecture Notes in Computer Science, pages 332–337, Jyväskylä, Finland, 1998. Springer-Verlag.
doi  abstract   bibtex   
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. Specifications using abstract statements scale up better than prepostconditions and allow for ‘relative’ specifications because they may refer to other components. 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 of any component market.
@inproceedings{BuchiSekerinski98Components,
	address = {Jyväskylä, Finland},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Formal {Methods} for {Component} {Software}: {The} {Refinement} {Calculus} {Perspective}},
	volume = {1357},
	doi = {10.1007/3-540-69687-3_68},
	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. Specifications using abstract statements scale up better than prepostconditions and allow for ‘relative’ specifications because they may refer to other components. 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 of any component market.},
	booktitle = {Object-{Oriented} {Technology}. {ECOOP} 1997},
	publisher = {Springer-Verlag},
	author = {Büchi, Martin and Sekerinski, Emil},
	editor = {Bosch, Jan and Mitchell, Stuart},
	year = {1998},
	pages = {332--337},
}

Downloads: 0