Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo


[4b23aa]: web / entries / MonoBoolTranAlgebra.shtml Maximize Restore History

Download this file

MonoBoolTranAlgebra.shtml    99 lines (81 with data), 3.3 kB

<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
  <title>Archive of Formal Proofs</title>
  <link rel="stylesheet" type="text/css" href="front.css">
  <link rel="icon" href="../images/favicon.ico" type="image/icon">
  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">

<table width="100%">
      <td width="20%" align="center" valign="top">
      <!-- navigation -->
      <!--#include file="nav.html"-->
      <td width="80%" valign="top">
      <!-- content -->

<div align="center">
<p> </p>

<h1><font class="first">A</font>lgebra
<font class="first">M</font>onotonic
<font class="first">B</font>oolean
<font class="first">T</font>ransformers
<table width="80%" class="data">
    <tr><td class="datahead" width="20%">Title:</td>
        <td class="data" width="80%">Algebra of Monotonic Boolean Transformers</td></tr>

    <tr><td class="datahead">Author:</td>
        <td class="data"><a href="http://users.abo.fi/vpreotea/">Viorel Preoteasa</a></td></tr>

    <tr><td class="datahead">Submission date:</td>
        <td class="data">2011-09-22</td></tr>

    <tr><td class="datahead" valign="top">Abstract:</td>
        <td class="abstract">

Algebras of imperative programming languages have been successful in reasoning about programs. In general an algebra of programs is an algebraic structure with programs as elements and with program compositions (sequential composition, choice, skip) as algebra operations. Various versions of these algebras were introduced to model partial correctness, total correctness, refinement, demonic choice, and other aspects. We formalize here an algebra which can be used to model total correctness, refinement, demonic and angelic choice. The basic model of this algebra are monotonic Boolean transformers (monotonic functions from a Boolean algebra to itself).

    <tr><td class="datahead">License:</td>
        <td class="data"><a href="http://afp.sourceforge.net/LICENSE">BSD License</a></td></tr>

<!--#set var="status" value="-STATUS-" -->
<!--#set var="version" value="-VERSION-" -->
<!--#set var="afp-version" value="-AFPVERSION-" -->
<!---INCLUDE- file="devel-warning.shtml"-->



<!--#set var="name" value="MonoBoolTranAlgebra" -->
<!--#set var="binfo" value="../browser_info/current/HOL/LatticeProperties/${name}" -->

<!--#set var="doc" value="${binfo}/document.pdf" -->
<!--#set var="outline" value="${binfo}/outline.pdf" -->
<!--#set var="browse" value="${binfo}/index.html" -->
<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->

<table class="links">
  <td class="links">
	<a href="<!--#echo var="outline" -->">Proof outline</a><br>
	<a href="<!--#echo var="doc" -->">Proof document</a>
	<!-- link to README.hmtl if no document exists -->	
  <td class="links">
	<a href="<!--#echo var="browse" -->">Browse theories</a>
  <td class="links"> 
	<a href="<!--#echo var="tar" -->">Download this entry</a>
    <tr><td class="links">Older releases:
None    </td></tr>
<!-- entry data end -->

</td> </tr> </table>