Automated Algebraic Reasoning for Collections and Local Variables with Lenses

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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
Original languageEnglish
Title of host publication18th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2020)
Number of pages16
Publication statusPublished - 1 Apr 2020

Publication series

NameLecture Notes in Computer Science

Bibliographical note

© 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.

Cite this