Overview

Version 7 (Stefan Blom, 20 Jul 2012 12:03)

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 5 Stefan Blom
Command line building uses Apache ant.
88 5 Stefan Blom
To build the toolset got to the root directory and enter the command 
89 5 Stefan Blom
<pre>
90 5 Stefan Blom
ant
91 5 Stefan Blom
</pre>
92 5 Stefan Blom
To create a distribution enter
93 5 Stefan Blom
<pre>
94 5 Stefan Blom
ant dist
95 5 Stefan Blom
</pre>
96 5 Stefan Blom
97 5 Stefan Blom
h2. Setting up for eclipse development.
98 5 Stefan Blom
99 6 Stefan Blom
See also [[Eclipse Setup]]
100 6 Stefan Blom
101 5 Stefan Blom
The VerCors tool set is split into several modules, which have to be configured as eclipse projects.
102 5 Stefan Blom
103 5 Stefan Blom
h3. Hybrid Runtime Environment (hre)
104 5 Stefan Blom
105 5 Stefan Blom
depends on: - 
106 5 Stefan Blom
107 5 Stefan Blom
This module contains functionality that has uses outside of the VerCors toolset.
108 5 Stefan Blom
109 5 Stefan Blom
h3. Core Data Structures (core)
110 5 Stefan Blom
111 5 Stefan Blom
depends on: hre
112 5 Stefan Blom
113 5 Stefan Blom
This module contains the main data structures for the VerCors toolset:
114 5 Stefan Blom
* the Common Object Language (COL) Abstract Syntax Tree.
115 5 Stefan Blom
* Pretty printing framework.
116 5 Stefan Blom
* Visitor Patterns for AST.
117 5 Stefan Blom
118 5 Stefan Blom
h3. Main program (main)
119 5 Stefan Blom
120 5 Stefan Blom
depends on: hre, core
121 5 Stefan Blom
122 5 Stefan Blom
The main program of the VerCors verifier Tool (vct).
123 5 Stefan Blom
124 5 Stefan Blom
h3. Java Parser plugin (java-parser)
125 5 Stefan Blom
126 5 Stefan Blom
depends on: hre, core
127 5 Stefan Blom
128 5 Stefan Blom
Parser for Java, written with the JavaCC 5.0 parser generator.
129 5 Stefan Blom
130 5 Stefan Blom
To compile this parser plugin, you may:
131 5 Stefan Blom
* Perform a command line build using ant.
132 5 Stefan Blom
* Perform an eclipse build using the eclipse ant builder.
133 5 Stefan Blom
* Install and use the JavaCC eclipse plugin.
134 5 Stefan Blom
135 5 Stefan Blom
h3. PVL Parser plugin (pvl-parser)
136 5 Stefan Blom
137 5 Stefan Blom
depends on: hre, core
138 5 Stefan Blom
139 5 Stefan Blom
Parser for PVL (toy language used in the program verification course), written with the ANTLR 3.4 parser generator.
140 5 Stefan Blom
141 5 Stefan Blom
To compile this parser plugin, you may:
142 5 Stefan Blom
* Perform a command line build using ant.
143 5 Stefan Blom
* Perform an eclipse build using the eclipse ant builder.
144 5 Stefan Blom
* Install and use the ANTLR v3 eclipse plugin.