[isabelle] new in the AFP: pGCL
- To: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] new in the AFP: pGCL
- From: Gerwin Klein <Gerwin.Klein at nicta.com.au>
- Date: Mon, 14 Jul 2014 15:10:27 +0000
- Accept-language: en-AU, en-US
- Thread-index: AQHPn3W+fuq11Dm+Bki4Qp6lWedLVA==
- Thread-topic: new in the AFP: pGCL
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.
As presented this morning at ITP’14.
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and