Email Gateway (Aug 19 2022 at 14:52): Email Gateway (Aug 19 2022 at 14:52):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
New in the AFP:
pGCL in Isabelle
by David Cock
pGCL is both a programming language and a specification language that incorporates both probabilistic and nondeterministic choice, in a unified manner. Program verification is by refinement or annotation (or both), using either Hoare triples, or weakest-precondition entailment, in the style of GCL.
This package provides both a shallow embedding of the language primitives, and an annotation and refinement framework. The generated document includes a brief tutorial.
http://afp.sourceforge.net/entries/pGCL.shtml
As presented this morning at ITP’14.
Enjoy!
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC