TY - GEN
T1 - Operational Annotations
T2 - 14th International Symposium on NASA Formal Methods, NFM 2022
AU - Attie, Paul C.
N1 - Publisher Copyright:
© 2022, Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - I present a new method for specifying and verifying the partial correctness of sequential programs. The key observation is that, in Hoare logic, assertions are used as selectors of states, that is, an assertion specifies the set of program states that satisfy the assertion. Hence, the usual meaning of the partial correctness Hoare triple {f}P{g} : if execution is started in any of the states that satisfy assertion f, then, upon termination, the resulting state will be some state that satisfies assertion g. There are of course other ways to specify a set of states. Given a program α, the post-states of α are the states that α may terminate in, given that α starts executing in an arbitrary initial state. I introduce the operational triple [α]P[β] to mean: if execution of P is started in any post-state of α, then upon termination, the resulting state will be some post-state of β. Here, α is the pre-program, and plays the role of a pre-condition, and β is the post-program, and plays the role of a post-condition.
AB - I present a new method for specifying and verifying the partial correctness of sequential programs. The key observation is that, in Hoare logic, assertions are used as selectors of states, that is, an assertion specifies the set of program states that satisfy the assertion. Hence, the usual meaning of the partial correctness Hoare triple {f}P{g} : if execution is started in any of the states that satisfy assertion f, then, upon termination, the resulting state will be some state that satisfies assertion g. There are of course other ways to specify a set of states. Given a program α, the post-states of α are the states that α may terminate in, given that α starts executing in an arbitrary initial state. I introduce the operational triple [α]P[β] to mean: if execution of P is started in any post-state of α, then upon termination, the resulting state will be some post-state of β. Here, α is the pre-program, and plays the role of a pre-condition, and β is the post-program, and plays the role of a post-condition.
KW - Hoare logic
KW - Program verification
UR - http://www.scopus.com/inward/record.url?scp=85131150343&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85131150343&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-06773-0_32
DO - 10.1007/978-3-031-06773-0_32
M3 - Conference contribution
AN - SCOPUS:85131150343
SN - 9783031067723
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 597
EP - 615
BT - NASA Formal Methods - 14th International Symposium, NFM 2022, Proceedings
A2 - Deshmukh, Jyotirmoy V.
A2 - Havelund, Klaus
A2 - Perez, Ivan
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 24 May 2022 through 27 May 2022
ER -