CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

A Hoare logic for the state monad: Proof pearl

Wouter Swierstra (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
Lecture Notes in Computer Science: 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009; Munich; Germany; 17 August 2009 through 20 August 2009 (03029743). Vol. 5674 LNCS (2009), p. 440-451.
[Konferensbidrag, refereegranskat]

This pearl examines how to verify functional programs written using the state monad. It uses Coq's Program framework to provide strong specifications for the standard operations that the state monad supports, such as return and bind. By exploiting the monadic structure of such programs during the verification process, it becomes easier to prove that they satisfy their specification.



Denna post skapades 2017-12-01.
CPL Pubid: 253478

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers) (2008-2010)

Ämnesområden

Data- och informationsvetenskap

Chalmers infrastruktur