On the Refinement Calculus
作者： Trevor Vickers , Carroll Morgan
DOI:
关键词:
摘要: The Specification Statement.- 1 Introduction.- 2 statements.- 3 implementation ordering.- 4 Suitability of the definitions.- 5 Using specification 6 Miracles.- 7 Guarded commands are miracles.- 8 Positive applications 9 Conclusion.- 10 Acknowledgements.- Statements and Refinement.- refinement theorems.- calculus.- An example: square root.- Derivation laws.- Procedures, Parameters, Abstraction: Separate Concerns.- Procedure call.- Procedural abstraction.- Parameters.- Data Refinement by abstract program.- A difficult data refinement.- Miraculous programs.- Eliminating Auxiliary Variables in direct technique.- auxiliary variable correspondence.- Predicate Transformers.- transformers.- Algorithmic predicate programming language.- Distribution specifications.- practice.- Conclusions.- Calculation.- Language extensions.- calculators.- Example refinement: "mean" module.- Specialized techniques.- Appendix: Single Complete Rule for Completeness.- Soundness.- Partial example.- Types Invariants Calculus.- Invariant semantics.- development method.- Laws local invariants.- Type-checking.- Recursion.- Examples.- discussion motives.- 11 Related work.- 12 Additional References.- Authors' Addresses.
amazon.com
springer.com
acm.org 参考文章(21)
J. M. Morris, Laws of data refinement Acta Informatica. ,vol. 26, pp. 287- 308 ,(1989) , 10.1007/BF00276019
J. R. Abrial, A Formal Approach To Large Software Construction mathematics of program construction. pp. 1- 20 ,(1989) , 10.1007/3-540-51305-1_1
Richard S. Bird, An introduction to the theory of lists Proceedings of the NATO Advanced Study Institute on Logic of programming and calculi of discrete design. pp. 5- 42 ,(1987) , 10.1007/978-3-642-87374-4_1
Ian James Hayes, Bill Flinn, Roger Gimson, Specification case studies Prentice Hall International (UK) Ltd.. ,(1987)
C B Jones, Systematic software development using VDM Prentice Hall International (UK) Ltd.. ,(1986)
Mark B. Josephs, The data refinement calculator for Z specifications Information Processing Letters. ,vol. 27, pp. 29- 33 ,(1988) , 10.1016/0020-0190(88)90078-6
Carroll Morgan, The specification statement ACM Transactions on Programming Languages and Systems. ,vol. 10, pp. 403- 419 ,(1988) , 10.1145/44501.44503
Greg Nelson, A generalization of Dijkstra's calculus ACM Transactions on Programming Languages and Systems. ,vol. 11, pp. 517- 561 ,(1989) , 10.1145/69558.69559
David Gries, Gary Levin, Assignment and Procedure Call Proof Rules ACM Transactions on Programming Languages and Systems. ,vol. 2, pp. 564- 579 ,(1980) , 10.1145/357114.357119
N. Wirth, Programming in Modula-2 ,(1982)