<?xml version="1.0"?>
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="cs" lang="cs"><!-- InstanceBegin template="/Templates/template.dwt" codeOutsideHTMLIsLocked="false" -->
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8" />
<meta http-equiv="content-language" content="cs" />
<meta name="robots" content="all,follow" />
<meta name="author" content="All: ... [Nazev webu - www.url.cz]; e-mail: info@url.cz" />
<meta name="copyright" content="Design/Code: Vit Dlouhy [Nuvio - www.nuvio.cz]; e-mail: vit.dlouhy@nuvio.cz" />
<!-- InstanceBeginEditable name="doctitle" -->
<title>Documentation</title>
<!-- InstanceEndEditable -->
<meta name="description" content="..." />
<meta name="keywords" content="..." />
<link rel="index" href="../." title="Home" />
<link rel="stylesheet" media="screen,projection" type="text/css" href="css/main.css" />
<link rel="stylesheet" media="print" type="text/css" href="css/print.css" />
<link rel="stylesheet" media="aural" type="text/css" href="css/aural.css" />
<!-- InstanceBeginEditable name="head" --><!-- InstanceEndEditable -->
</head>
<body id="www-url-cz">
<!-- Main -->
<div id="main" class="box">
<!-- Header -->
<div id="header">
<!-- Logotyp -->
<h1 id="logo" title="Integrating Z and B tools with SMT-solvers">ZB2SMT</h1>
<hr class="noscreen" />
</div> <!-- /header -->
<!-- Main menu (tabs) -->
<div id="tabs" class="noprint">
<h3 class="noscreen">Navigation</h3>
<ul class="box">
<li id="active"><a href="index.html">Home<span class="tab-l"></span><span class="tab-r"></span></a></li>
<li><a href="download.html">Download<span class="tab-l"></span><span class="tab-r"></span></a></li>
<li><a href="doc.html">Documentation<span class="tab-l"></span><span class="tab-r"></span></a></li>
<li><a href="people.html">People<span class="tab-l"></span><span class="tab-r"></span></a></li>
<li><a href="support.html">Support<span class="tab-l"></span><span class="tab-r"></span></a></li>
<li><a href="links.html">Related Links<span class="tab-l"></span><span class="tab-r"></span></a></li>
</ul>
<hr class="noscreen" />
</div> <!-- /tabs -->
<!-- Page (2 columns) -->
<div id="page" class="box">
<div id="page-in" class="box">
<!-- Content -->
<!-- InstanceBeginEditable name="content" -->
<div id="content">
<!-- Article -->
<div class="article">
<h2><span>Documentation</span></h2>
<br />
<h3><span>How to Install</span></h3>
<p> Unpackage the zb2smt version. There are two files, zb2smt.jar and server.jar. The former is the ZB2SMT library containing the classes that will take the Z (inside, Z predicates are converted to B predicates) or B predicates, transform into SMT files and execute the propers SMT solvers. This jar has to be included in your tool build path project.
</p>
<p> The latter, server.jar, is used to distribute the execution of solvers. It is responsible for the server side and is described later in the section <a href="doc.html#Distributing proofs">Distributing proofs</a>. Finally, the folder smt-solvers contains
the theorem provers that are currently integrated and can be accessed directly by the package ZB2SMT. It also has a Config used in the distributing procces to configure the client. The smt-folders has to be in the folder of the tool project in order to be correctly used.
<h3><span>Using zb2smt</span></h3>
<p> ZB2SMT has proper methods to get a boolean answer from a smt-solver in proof of some predicate. The class zb2smt.ZB2SMTUtils.Java is a facade to its methods. In order to prove some predicate using the ZB2SMT package, you can invoke ZB2SMTUTils.proveBySMTProver(predicate), where *SMTProver can be: veriT, z3, Yices, CVC3, Alt-Ergo. The availability of its solvers is it as follow.
</p>
<p> Windows: veriT, Yices and Z3</p>
<p> Linux: veriT, Yices, Alt-Ergo and CVC3</p>
<p> The package also can be used to get the SMT pure file corresponding a predicate. This file can be sent to others SMT solvers that are not yet available in the package. To create the file or get the body text of it use the methods generatePureSMTfile(pred).</p>
<h3><span>Limitations</span></h3>
<p> Inside ZB2SMT, Z predicates are converted to B predicates, using the extension of BOL. The extension is needed due to the fact that there are Z operators that do not exist in BOL like the symmetric difference operator. Extending BOL by including these missing operators, we improve the set of predicates that can be treated by our package. These predicates are translated into a SMT syntax and written to a file that contains the predicate and some elements such as types of variables, operators definition and set properties that are described over the macro feature of veriT. You can download <a href="doc/operatosdoc.pdf" style="color:#0099FF">Here</a> a document about these operators.</p>
<h3><span>Paralleling Proof Executions</span></h3>
<p> The ZBS2MT has a module that can call differents instance of theorem provers at differents computers, using sockets and threads. This module has two parts: the client with the information about each possible instance of theorem
prover, which can be local or remote, and the server with the theorem prover installed locally.</p>
<p> In order to use this feature, some steps are needed. Next, we describe each one of them.</p>
<ol>
<li> Start the Proof Server</li>
- Use the command: " java -jar server.jar". Note that, server.jar and zb2smt.jar comes together in the zip file available for download; <br>
- Or use direclty the methods from "network.server.ProofServer";
<li> Configure the file called Config found in the smt-solvers folder</li>
- Config file contains a list of hostnames and paths for the solvers. You have to configure puting the IP address of the machine and the absolute path of the prover that you want to be executed. See the example below.<br />
<br />
/bin/cvc -lang smt@10.91.98.101 <br />
/user/workspace/toolproject/smt-solvers/veriT/linux/rv@127.0.0.1 <br />
/user/workspace/toolproject/smt-solvers/cvc3/cvc3-optimized -lang smtlib@127.0.0.1<br />
C:\Users\toolproject\smt-solvers\z3\z3.exe@10.9.98.123*(Windows)<br />
* Use the IP 127.0.0.1 to execute locally.
<br />
<br />
<li> This feature is ready to be used. Use the method zb2smt.ZB2SMTUTils.executeAccordingConfig(pred) to
execute this functionality. </li>
</ol>
<br/>
</div>
<!-- /article -->
<hr class="noscreen" />
<hr class="noscreen" />
</div>
<!-- /content -->
<!-- InstanceEndEditable -->
<!-- Right column -->
<div id="col" class="noprint">
<div id="col-in">
<!-- Links -->
<h3><span>Links</span></h3>
<p> <a href="http://sites.google.com/site/forallufrn/"> <img src="figures/ufrn.jpg" width="100" height="37"/> </a></p>
<p> <a href="http://www.dimap.ufrn.br/" > <img src="figures/logo_dimap.gif" width="100" height="37" /> </a> </p>
<p> <a href="http://www.ccet.ufrn.br/prh22/frame.htm"> <img src="figures/simb_PRH2.gif" width="100" height="37" /> </a> </p>
<hr class="noscreen" />
</div> <!-- /col-in -->
</div> <!-- /col -->
</div> <!-- /page-in -->
</div> <!-- /page -->
<!-- Footer -->
<div id="footer">
<hr class="noscreen" />
<p id="createdby">created by <a href="http://www.nuvio.cz">Nuvio | Webdesign</a> <!-- DON´T REMOVE, PLEASE! --></p>
<p id="copyright">© 2010 <a href="mailto:alessandrogurgel@gmail.com">Alessandro Gurgel</a></p>
</div> <!-- /footer -->
</div> <!-- /main -->
</body>
<!-- InstanceEnd --></html>