TY - CHAP
T1 - Invariant patterns for program reasoning
AU - Ireland, Andrew
AU - Ellis, William James
AU - Ingulfsen, Tommy
PY - 2004
Y1 - 2004
N2 - We address the problem of integrating standard techniques for automatic invariant generation within the context of program reasoning. We propose the use of invariant patterns which enable us to associate common patterns of program code and specifications with invariant schemas. This allows crucial decisions relating to the development of invariants to be delayed until a proof is attempted. Moreover, it allows patterns within the program to be exploited in patching failed proof attempts.
AB - We address the problem of integrating standard techniques for automatic invariant generation within the context of program reasoning. We propose the use of invariant patterns which enable us to associate common patterns of program code and specifications with invariant schemas. This allows crucial decisions relating to the development of invariants to be delayed until a proof is attempted. Moreover, it allows patterns within the program to be exploited in patching failed proof attempts.
UR - http://www.scopus.com/inward/record.url?scp=9444232287&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-24694-7_20
DO - 10.1007/978-3-540-24694-7_20
M3 - Chapter (peer-reviewed)
SN - 978-3-540-21459-5
VL - 2972
T3 - Lecture Notes in Computer Science
SP - 190
EP - 201
BT - MICAI 2004: Advances in Artificial Intelligence
T2 - Third Mexican International Conference on Artificial Intelligence
Y2 - 26 April 2004 through 30 April 2004
ER -