Mark Utting

https://researchers.uq.edu.au/researcher/26046 [email protected]

The University of Queensland Research interests: software verification; theorem proving; model-based testing; language design; blockchain

Repositories
Issues
Comments

Results 1 comments of


                                            Mark Utting

Overlapping Lvals

If you want to allow overlapping lvals, I think it should generate a proof obligation: assert i != j; or perhaps more generally: assert i == j ==> rhs1 ==...