Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: README.html Sprache: HTML

Original von: Isabelle^©

products/sources/formale Sprachen/Isabelle/HOL/UNITY/Comp/README.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

<HTML>

<HEAD>
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
  <TITLE>HOL/UNITY/README</TITLE>
</HEAD>

<BODY>

<H2>UNITY: Examples Involving Program Composition</H2>

<P>
The directory presents verification examples involving program composition.
They are mostly taken from the works of Chandy, Charpentier and Chandy.

<UL>
<LI>examples of <em>universal properties</em>:
the counter (<A HREF="Counter.thy"><CODE>Counter.thy</CODE></A>)
and priority system (<A HREF="Priority.thy"><CODE>Priority.thy</CODE></A>)

<LI>the allocation system (<A HREF="Alloc.thy"><CODE>Alloc.thy</CODE></A>)

<LI>client implementation (<A HREF="Client.thy"><CODE>Client.thy</CODE></A>)

<LI>allocator implementation (<A HREF="AllocImpl.thy"><CODE>AllocImpl.thy</CODE></A>)

<LI>the handshake protocol
(<A HREF="Handshake.thy"><CODE>Handshake.thy</CODE></A>)

<LI>the timer array (demonstrates arrays of processes)
(<A HREF="TimerArray.thy"><CODE>TimerArray.thy</CODE></A>)
</UL>

<P> Safety proofs (invariants) are often proved automatically.  Progress
proofs involving ENSURES can sometimes be proved automatically.  The
level of automation appears to be about the same as in HOL-UNITY by Flemming
Andersen et al.

<ADDRESS>
<A NAME="[email protected]" HREF="mailto:[email protected]">[email protected]</A>
</ADDRESS>
</BODY>
</HTML>

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.