Automated Algebraic Reasoning for Collections and Local Variables with Lenses

TY - GEN

T1 - Automated Algebraic Reasoning for Collections and Local Variables with Lenses

AU - Foster, Simon David

AU - Baxter, James

N1 - © Springer Nature Switzerland AG 2020. This is an author-produced version of the published paper. Uploaded in accordance with the publisher’s self-archiving policy. Further copying may not be permitted; contact the publisher for details.

PY - 2020/4/1

Y1 - 2020/4/1

N2 - Lenses are a useful algebraic structure for giving a unifying semantics to program variables in a variety of store models. They support efficient automated proof in the Isabelle/UTP verification framework. In this paper, we expand our lens library with (1) dynamic lenses, that support mutable indexed collections, such as arrays, and (2) symmetric lenses, that allow partitioning of a state space into disjoint local and global regions to support variable scopes. From this basis, we provide an enriched program model in Isabelle/UTP for collection variables and variable blocks. For the latter, we adopt an approach first used by Back and von Wright, and derive weakest precondition and Hoare calculi. We demonstrate several examples, including verification of insertion sort

AB - Lenses are a useful algebraic structure for giving a unifying semantics to program variables in a variety of store models. They support efficient automated proof in the Isabelle/UTP verification framework. In this paper, we expand our lens library with (1) dynamic lenses, that support mutable indexed collections, such as arrays, and (2) symmetric lenses, that allow partitioning of a state space into disjoint local and global regions to support variable scopes. From this basis, we provide an enriched program model in Isabelle/UTP for collection variables and variable blocks. For the latter, we adopt an approach first used by Back and von Wright, and derive weakest precondition and Hoare calculi. We demonstrate several examples, including verification of insertion sort

U2 - 10.1007/978-3-030-43520-2_7

DO - 10.1007/978-3-030-43520-2_7

M3 - Conference contribution

T3 - Lecture Notes in Computer Science

BT - 18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020)

PB - Springer

ER -