Overview

Version 9 (Stefan Blom, 03 Oct 2012 14:45)

1 1 Stefan Blom
h1. Overview
2 1 Stefan Blom
3 3 Stefan Blom
The "VerCors project":http://fmt.ewi.utwente.nl/research/projects/VerCors/ is about Verification of Concurrent Data Structures.
4 1 Stefan Blom
5 1 Stefan Blom
The VerCors toolset currently consists of two tools:
6 2 Stefan Blom
* "Histogram":http://fmt.ewi.utwente.nl/tools/histogram: a tool for creating Histograms of class/method occurrences.
7 2 Stefan Blom
* [[Verifier Overview|The VerCors verifier]]: an annotated code compiler/verifier.
8 4 Stefan Blom
9 5 Stefan Blom
h1. Binary Distribution
10 1 Stefan Blom
11 5 Stefan Blom
This chapter is about installing the binary version.
12 5 Stefan Blom
13 1 Stefan Blom
h2. Prerequisites
14 1 Stefan Blom
15 5 Stefan Blom
To run the binary version, you will need a Java Runtime Environment.
16 5 Stefan Blom
Note that the toolset has been tested with the Oracle Java 1.6 SE SDK.
17 5 Stefan Blom
Compatibility with other JVMs is untested.
18 5 Stefan Blom
19 5 Stefan Blom
h3. Windows
20 5 Stefan Blom
21 5 Stefan Blom
The binary distribution requires no non-standard components.
22 5 Stefan Blom
23 5 Stefan Blom
h3. Linux and MacOSX
24 5 Stefan Blom
25 5 Stefan Blom
The following two packages are needed:
26 5 Stefan Blom
27 5 Stefan Blom
* wine (no known version requirements)
28 5 Stefan Blom
* mono (2.10 or better)
29 5 Stefan Blom
30 5 Stefan Blom
*Linux notes*
31 5 Stefan Blom
32 5 Stefan Blom
All common Linux distributions include a package for wine, so it may be installed using the package manager of your distribution.
33 5 Stefan Blom
Not all common Linux distributions include a sufficiently up-to-date version of mono. Thus you may need to download sources from
34 5 Stefan Blom
http://www.mono-project.com/ and follow instructions on how to compile them.
35 5 Stefan Blom
36 5 Stefan Blom
*MacOSX notes*
37 5 Stefan Blom
38 5 Stefan Blom
Unfortunately, we do not know of any binary distribution of wine on MacOSX.
39 5 Stefan Blom
Thus, we recommend installing macports (http://www.macports.org/) and then installing wine:
40 5 Stefan Blom
<pre>
41 5 Stefan Blom
sudo port install wine
42 5 Stefan Blom
</pre>
43 5 Stefan Blom
44 5 Stefan Blom
For installing mono, you have two options:
45 5 Stefan Blom
# Get a binary distribution from http://www.mono-project.com/
46 5 Stefan Blom
# Install using macports:
47 5 Stefan Blom
<pre>
48 5 Stefan Blom
sudo port install mono???
49 5 Stefan Blom
</pre>
50 5 Stefan Blom
51 5 Stefan Blom
52 5 Stefan Blom
h2. Installation.
53 5 Stefan Blom
54 5 Stefan Blom
# Download the zip archive with the binary distribution. E.g. @vct-1.0.zip@.
55 5 Stefan Blom
# Extract the files from the zip archive.
56 5 Stefan Blom
# For easy command line access: add the bin subdirectory to your PATH variable.
57 5 Stefan Blom
58 5 Stefan Blom
h1. Source Distribution.
59 5 Stefan Blom
60 5 Stefan Blom
The source distribution has been structured to allow both command line building with ant and development with eclipse.
61 5 Stefan Blom
62 5 Stefan Blom
h2. Getting the sources.
63 5 Stefan Blom
64 5 Stefan Blom
There are two ways to get the sources:
65 5 Stefan Blom
66 5 Stefan Blom
# Download a zip archive.
67 5 Stefan Blom
# Clone one of the git repositories.
68 5 Stefan Blom
69 5 Stefan Blom
h3. Git repositories.
70 7 Stefan Blom
71 7 Stefan Blom
See [[Installing git for windows]].
72 7 Stefan Blom
73 5 Stefan Blom
* EWI compute server demeter.
74 5 Stefan Blom
>> URL: demeter.ewi.utwente.nl:/home/sccblom/git/vercors-toolset.git
75 5 Stefan Blom
>> access: UTwente AD password, you can setup key logins if you like. This repository is read-only, to upload changes you need to create you own repository.
76 5 Stefan Blom
* Temporary SSH based git server.
77 5 Stefan Blom
>> URL: gitshare@sccblom.ewi.utwente.nl:vercors-toolset.git
78 5 Stefan Blom
>> access: create an SSH key pair and email the public key to Stefan. This repository is read/write. 
79 5 Stefan Blom
80 5 Stefan Blom
Note that the git repositories have submodules. That is, after cloning one of the git repositories, you must initialize the sub modules:
81 5 Stefan Blom
<pre>
82 5 Stefan Blom
git submodule update --init
83 5 Stefan Blom
</pre>
84 5 Stefan Blom
85 5 Stefan Blom
h2. Command line building.
86 5 Stefan Blom
87 9 Stefan Blom
Command line building uses Apache ant. To build the tool set go to the root directory and enter the command 
88 5 Stefan Blom
<pre>
89 5 Stefan Blom
ant
90 5 Stefan Blom
</pre>
91 5 Stefan Blom
To create a distribution enter
92 5 Stefan Blom
<pre>
93 5 Stefan Blom
ant dist
94 5 Stefan Blom
</pre>
95 5 Stefan Blom
96 1 Stefan Blom
h2. Overview of the Modules of the VerCors Tool set
97 8 Stefan Blom
98 9 Stefan Blom
The VerCors tool set is split into several modules plus scripts to make everything work together. You cannot use eclipse to manage the VerCors tool set. You can use eclipse to work on each module. For detailed configuration instructions for eclipse see [[Eclipse Setup]].
99 8 Stefan Blom
100 9 Stefan Blom
Next, we will give an overview of the modules. The name of the subdirectory of the module is given between parenthesis.
101 5 Stefan Blom
102 5 Stefan Blom
h3. Hybrid Runtime Environment (hre)
103 5 Stefan Blom
104 5 Stefan Blom
depends on: - 
105 5 Stefan Blom
106 5 Stefan Blom
This module contains functionality that has uses outside of the VerCors toolset.
107 5 Stefan Blom
108 5 Stefan Blom
h3. Core Data Structures (core)
109 5 Stefan Blom
110 5 Stefan Blom
depends on: hre
111 5 Stefan Blom
112 5 Stefan Blom
This module contains the main data structures for the VerCors toolset:
113 5 Stefan Blom
* the Common Object Language (COL) Abstract Syntax Tree.
114 5 Stefan Blom
* Pretty printing framework.
115 5 Stefan Blom
* Visitor Patterns for AST.
116 5 Stefan Blom
117 5 Stefan Blom
h3. Main program (main)
118 5 Stefan Blom
119 5 Stefan Blom
depends on: hre, core
120 5 Stefan Blom
121 5 Stefan Blom
The main program of the VerCors verifier Tool (vct).
122 5 Stefan Blom
123 5 Stefan Blom
h3. Java Parser plugin (java-parser)
124 5 Stefan Blom
125 5 Stefan Blom
depends on: hre, core
126 5 Stefan Blom
127 5 Stefan Blom
Parser for Java, written with the JavaCC 5.0 parser generator.
128 5 Stefan Blom
129 5 Stefan Blom
To compile this parser plugin, you may:
130 5 Stefan Blom
* Perform a command line build using ant.
131 5 Stefan Blom
* Perform an eclipse build using the eclipse ant builder.
132 5 Stefan Blom
* Install and use the JavaCC eclipse plugin.
133 5 Stefan Blom
134 5 Stefan Blom
h3. PVL Parser plugin (pvl-parser)
135 5 Stefan Blom
136 5 Stefan Blom
depends on: hre, core
137 5 Stefan Blom
138 5 Stefan Blom
Parser for PVL (toy language used in the program verification course), written with the ANTLR 3.4 parser generator.
139 5 Stefan Blom
140 5 Stefan Blom
To compile this parser plugin, you may:
141 5 Stefan Blom
* Perform a command line build using ant.
142 5 Stefan Blom
* Perform an eclipse build using the eclipse ant builder.
143 5 Stefan Blom
* Install and use the ANTLR v3 eclipse plugin.