Abstract
This chapter is the first of Part IV, in which propose a compositional verification method to derive a correctness formula for a rule program from individual correctness formulas for its rules. This verification method is composed of several proof rules that are suited to various types of rule programs and assertions. In the present chapter, we introduce a simpler proof rule for a particular class of rule programs, so as to exhibit the core mechanism at play.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Apt, K.R., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 2nd edn. Texts in Computer Science. Springer, Berlin (1997)
Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd edn. Texts in Computer Science. Springer, Berlin (2009)
Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Software Eng. 3(2), 125–143 (1977)
Lipton, R.J.: Reduction: A method of proving properties of parallel programs. Comm. ACM 18(12), 717–721 (1975)
Morris, J.M.: A general axiom of assignment. In: Bauer, F.L., Dijkstra, E.W., Hoare, C.A.R. (eds.) Theoretical Foundations of Programming Methodology: Lecture Notes of an International Summer School. Reidel, Dordrecht (1982)
Owicki, S.S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Informatica 6, 319–340 (1976)
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Berstel-Da Silva, B. (2014). Main Steps in Rule Program Verification. In: Verification of Business Rules Programs. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40038-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-40038-4_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-40037-7
Online ISBN: 978-3-642-40038-4
eBook Packages: Computer ScienceComputer Science (R0)