TY - GEN
T1 - Whither Specifications as Programs
AU - Naumann, David A.
AU - Ngo, Minh
N1 - Publisher Copyright:
© 2019, Springer Nature Switzerland AG.
PY - 2019
Y1 - 2019
N2 - Unifying theories distil common features of programming languages and design methods by means of algebraic operators and their laws. Several practical concerns—e.g., improvement of a program, conformance of code with design, correctness with respect to specified requirements—are subsumed by the beautiful notion that programs and designs are special forms of specification and their relationships are instances of logical implication between specifications. Mathematical development of this idea has been fruitful but limited to an impoverished notion of specification: trace properties. Some mathematically precise properties of programs, dubbed hyperproperties, refer to traces collectively. For example, confidentiality involves knowledge of possible traces. This article reports on both obvious and surprising results about lifting algebras of programming to hyperproperties, especially in connection with loops, and suggests directions for further research. The technical results are: a compositional semantics, at the hyper level, of imperative programs with loops, and proof that this semantics coincides with the direct image of a standard semantics, for subset closed hyperproperties.
AB - Unifying theories distil common features of programming languages and design methods by means of algebraic operators and their laws. Several practical concerns—e.g., improvement of a program, conformance of code with design, correctness with respect to specified requirements—are subsumed by the beautiful notion that programs and designs are special forms of specification and their relationships are instances of logical implication between specifications. Mathematical development of this idea has been fruitful but limited to an impoverished notion of specification: trace properties. Some mathematically precise properties of programs, dubbed hyperproperties, refer to traces collectively. For example, confidentiality involves knowledge of possible traces. This article reports on both obvious and surprising results about lifting algebras of programming to hyperproperties, especially in connection with loops, and suggests directions for further research. The technical results are: a compositional semantics, at the hyper level, of imperative programs with loops, and proof that this semantics coincides with the direct image of a standard semantics, for subset closed hyperproperties.
UR - http://www.scopus.com/inward/record.url?scp=85076118734&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85076118734&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-31038-7_3
DO - 10.1007/978-3-030-31038-7_3
M3 - Conference contribution
AN - SCOPUS:85076118734
SN - 9783030310370
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 39
EP - 61
BT - Unifying Theories of Programming - 7th International Symposium, UTP 2019, Dedicated to Tony Hoare on the Occasion of His 85th Birthday, Proceedings
A2 - Ribeiro, Pedro
A2 - Sampaio, Augusto
T2 - 7th International Symposium on Unifying Theories of Programming, UTP 2019
Y2 - 8 October 2019 through 8 October 2019
ER -