source: CIVL/src/overview.html@ e64170d

1.23 2.0 main test-branch
Last change on this file since e64170d was a01e883, checked in by Manchun Zheng <zmanchun@…>, 12 years ago

cleaned up Evaluator; improved javadocs.

git-svn-id: ​svn://vsl.cis.udel.edu/civl/trunk@1020 fb995dde-84ed-4084-dfe6-e5aef3e2452c
  • Property mode set to 100644
File size: 4.6 KB
Line 
1
2<html>
3<body>
4
5 <p>Welcome to CIVL, the Concurrency Intermediate Verification
6 Language tool. CIVL is a Java project for verifying concurrent
7 programs written in CIVL-C, which is a C dialect with extensions to
8 concurrent language constructs. The CIVL project uses ABC, SARL and
9 GMC. The CIVL tool can be used to perform a number of tasks, including
10 the following:
11 <ol>
12 <li>preprocess or pass a CIVL-C program;</i>
13 <li>verify a CIVL-C program;</li>
14 <li>run a CIVL-C program;</li>
15 <li>replay traces for a program.</li>
16 </ol>
17
18 In addition, it provides a framework for developing your own libraries
19 or transformations on ASTs of various language extensions and
20 libraries.
21 </p>
22
23 There is a simple command-line interface for CIVL (see {@link
24 edu.udel.cis.vsl.civl.CIVL CIVL}), but most users will want to use CIVL
25 through the user interface (see {@link
26 edu.udel.cis.vsl.civl.run.IF.UserInterface UserInterface}). To use the
27 API, it is helpful to have some understanding of the modular structure
28 of CIVL. The CIVL source code is decomposed into modules, each with a
29 well-defined interface and set of responsibilities. Some of these
30 modules are decomposed further into sub-modules. The top-level modules
31 are:
32 <ol>
33
34 <li><strong>util</strong>
35 <ol>
36 <li>responsibilities: simple general-purpose utility classes
37 that do not use other parts of CIVL</li>
38 <li>uses: nothing</li>
39 <li>interface: {@link edu.udel.cis.vsl.civl.util.IF}</li>
40 <li>entry point: none</li>
41 </ol></li>
42
43 <li><strong>transform</strong>
44 <ol>
45 <li>responsibilities: transformations of an AST</li>
46 <li>uses: <strong>abc</strong>, <strong>sarl</strong></li>
47 <li>interface: {@link edu.udel.cis.vsl.civl.transform.IF}</li>
48 <li>entry point: CIVLTransform</li>
49 </ol></li>
50
51 <li><strong>model</strong>
52 <ol>
53 <li>responsibilities: definitions of the control flow graph
54 representation of a CIVL-C program</li>
55 <li>uses: <strong>err</strong>, <strong>run</strong>, <strong>util</strong>,
56 <strong>abc</strong>, <strong>gmc</strong>, <strong>sarl</strong></li>
57 <li>interface: {@link edu.udel.cis.vsl.civl.model.IF}</li>
58 <li>entry point: Models</li>
59 <li>submodules
60 <ol>
61 <li><strong>expression</strong>
62 <ol>
63 <li>responsibilities: definitions of various expressions of
64 CIVL</li>
65 <li>interface: {@link
66 edu.udel.cis.vsl.civl.model.IF.expression}</li>
67 <li>entry point: none</li>
68 </ol></li>
69 <li><strong>location</strong>
70 <ol>
71 <li>responsibilities: definitions a location in the control
72 flow graph of a CIVL-C program</li>
73 <li>interface: {@link
74 edu.udel.cis.vsl.civl.model.IF.location}</li>
75 <li>entry point: none</li>
76 </ol></li>
77 <li><strong>statement</strong>
78 <ol>
79 <li>responsibilities: definitions of various statements of
80 CIVL</li>
81 <li>interface: {@link
82 edu.udel.cis.vsl.civl.model.IF.statement}</li>
83 <li>entry point: none</li>
84 </ol></li>
85 <li><strong>type</strong>
86 <ol>
87 <li>responsibilities: definitions of various types of CIVL</li>
88 <li>interface: {@link edu.udel.cis.vsl.civl.model.IF.type}</li>
89 <li>entry point: none</li>
90 </ol></li>
91 <li><strong>variable</strong>
92 <ol>
93 <li>responsibilities: definitions of a variable of CIVL</li>
94 <li>interface: {@link
95 edu.udel.cis.vsl.civl.model.IF.variable}</li>
96 <li>entry point: none</li>
97 </ol></li>
98 </ol>
99 </li>
100 </ol></li>
101
102 <li><strong>err</strong>
103 <ol>
104 <li>responsibilities: general exception classes that can be
105 thrown by CIVL.</li>
106 <li>uses: <strong>model</strong>, <strong>state</strong></li>
107 <li>interface: {@link edu.udel.cis.vsl.civl.err.IF}</li>
108 <li>entry point: none</li>
109 </ol></li>TBC.
110
111 <li><strong>run</strong>
112 <ol>
113 <li>responsibilities: parsing command line inputs and initial
114 configurations of the tool</li>
115 <li>uses: <strong>err</strong>, <strong>kripke</strong>, <strong>model</strong>,
116 <strong>state</strong>, <strong>transform</strong>, <strong>util</strong>,
117 <strong>abc</strong>, <strong>gmc</strong>, <strong>sarl</strong></li>
118 <li>interface: {@link edu.udel.cis.vsl.civl.run.IF}</li>
119 <li>entry point: UserInterface</li>
120 </ol></li>
121
122 <li><strong>main</strong>
123 <ol>
124 <li>responsibilities: parsing command line inputs and initial
125 configurations of the tool</li>
126 <li>uses: <strong>run</strong></li>
127 <li>interface: {@link edu.udel.cis.vsl.civl}</li>
128 <li>entry point: CIVL</li>
129 </ol></li>
130
131 </ol>
132
133</body>
134</html>
135
Note: See TracBrowser for help on using the repository browser.