Coalgebraic Reasoning about Classes in Object-Oriented Languages
Bart Jacobs · Electronic Notes in Theoretical Computer Science · 1998
This note briefly discusses how some of the ideas developed in the theory of coalgebras are used in a front-end tool called LOOP, developed jointly in Dresden and Nijmegen, for reasoning (with a back-end theorem prover) about classes in object-oriented languages. It will describe reasoning both about object-oriented specifications and about JAVA implementations, via examples.