-
Notifications
You must be signed in to change notification settings - Fork 0
/
instructions.html
353 lines (316 loc) · 17.1 KB
/
instructions.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
<!-- Instructions modal with instruction text -->
<div class="modal fade" id="info-modal" tabindex="-1" role="dialog" aria-labelledby="myModalLabel" aria-hidden="true">
<div class="modal-dialog">
<div class="modal-content">
<div class="modal-header">
<button type="button" class="close" data-dismiss="modal" aria-hidden="true">×</button>
<h4 class="modal-title" id="myModalLabel">Instructions</h4>
</div>
<div class="modal-body">
<div id="instructionGroup">
<div class="panel panel-danger panel-instruction">
<div class="panel-heading pointer collapsed" role="tab" id="headingAbout"
data-toggle="collapse" data-parent="#instructionGroup"
aria-expanded="true" aria-controls="collapseAbout" href="#collapseAbout">
<div class="panel-title">
<span class="glyphicon collapse-instruction"></span>
About
</div>
</div>
<div id="collapseAbout" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingAbout">
<div class="panel-body">
<h3>Purpose</h3>
The purpose of this application is to act as a program checker for a generic C-style
language. Upon receiving a given program, the program checker parses the program
and computes the formulas that need to be proven true so that the program can
be determined to be valid.
<h3>Workflow</h3>
For most programs to be checked by the program checker, it is simply necessary to
provide a precondition, the program itself, and a postcondition (More on preconditions
and postconditions in the following section). Clicking on the <strong>Submit</strong> button will
send the information to the program checker which will then verify and check the code.
Once this is done, the program checker will return its results. One of two things will
happen in this case.
<h4>The program is invalid</h4>
There will be an error displayed in the <strong>Proofs</strong> section indicating that the program
contains a syntax error. To help correct your code, please refer to the <strong>Program</strong> section
of the instructions.
<h4>The program is valid</h4>
The formulas needed to prove the validity of the program, given in propositional logic,
will be displayed in the <strong>Proofs</strong> section. Please note that some of these proofs may be
impossible to prove depending on the structure of the program and on the given precondition
and postcondition. It is up to the user to ensure that the pre- and postconditions are strong
enough to help complete the proofs.
</div>
</div>
</div>
<div class="panel panel-danger panel-instruction">
<div class="panel-heading pointer collapsed" role="tab" id="headingPrePost"
data-toggle="collapse" data-parent="#instructionGroup"
aria-expanded="true" aria-controls="collapsePrePost" href="#collapsePrePost">
<div class="panel-title">
<span class="glyphicon collapse-instruction"></span>
Precondition and Postcondition
</div>
</div>
<div id="collapsePrePost" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingPrePost">
<div class="panel-body">
The precondition and postcondition fields are used to specify what the program requires
to function correctly and what properties it guarantees that its output will have.
<h3>Precondition</h3>
The precondition is required for telling the program checker what the written program
needs to have guaranteed so that the program can then guarantee its own output. The
precondition can be anything the user wants, however for the program checker to be able
to properly manipulate it, it should be specified in propositional logic.
<h3>Postcondition</h3>
The postcondition is required for telling the program checker what the written program
guarantees that its output will hold the properties specified in the postcondition. Again, the
postcondition can be anything the user wants, however for the program checker to be able
to properly manipulate it, it should be specified in propositional logic.
<h3>Syntax</h3>
As previously mentioned, the pre- and postconditions can take any user input, however the
program checker can only manipulate them if they are specified in propositional logic. The
reason that the user has the freedom to specify anything is that it is sometimes useful for
the pre- and postconditions to specify complex or unique mathematic formulas. So, instead
of restricting the options, it was decided to give the user some freedom at the expense of
rigid validation. The user may therefore be able to specify any mathematical function or
expression of its choice, like x = f(y) or g! > sqrt(f!).
<h4>Symbols</h4>
Some symbols are recognized by the program checker. These symbols are output by the checker
in a way that makes them easier to read. The symbols that are recognized by the program checker
are the following:
<table class="table table-striped table-bordered">
<caption>List of symbols recognized by the program checker</caption>
<thead>
<tr>
<th>Group</th>
<th>Symbol</th>
<th>Program Checker Output</th>
</tr>
</thead>
<tbody>
<tr>
<th rowspan="4">Propositional Logic</th>
<td>-></td>
<td>→</td>
</tr>
<tr>
<td>/\</td>
<td>∧</td>
</tr>
<tr>
<td>\/</td>
<td>∨</td>
</tr>
<tr>
<td>~</td>
<td>¬</td>
</tr>
<tr>
<th rowspan="3">Mathematical</th>
<td>>=</td>
<td>≥</td>
</tr>
<tr>
<td><=</td>
<td>≤</td>
</tr>
<tr>
<td>!=</td>
<td>≠</td>
</tr>
</tbody>
</table>
In addition to these symbols, the symbols T and F represent tautology and contradiction,
respectively.
Any other symbols will be printed the same way as they were written in the pre- and
postcondition input boxes. For example, if the formula x = (y + 1)
is written in the precondition box, then it will be output the same way by the checker.
</div>
</div>
</div>
<div class="panel panel-danger panel-instruction">
<div class="panel-heading pointer collapsed" role="tab" id="headingProgram"
data-toggle="collapse" data-parent="#instructionGroup"
aria-expanded="true" aria-controls="collapseProgram" href="#collapseProgram">
<div class="panel-title">
<span class="glyphicon collapse-instruction"></span>
Program
</div>
</div>
<div id="collapseProgram" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingProgram">
<div class="panel-body">
The program to be checked by the program checker must be written in the program
text area. This is the code that will be analyzed by the checker and from which
the formulas whose validity needs to be proven are generated.
<h3>Syntax</h3>
<h4>BNF Notation</h4>
For quick reference, the program syntax follows the BNF notation described in chapter 4
of <em>Logic in Computer Science</em> by Michael Huth and Mark Ryan, second edition, on pages
260 - 261. In short, the context-free grammar accepted by the checker is the following:
<div class="well">
E ::= n | x | (-E) | (E + E) | (E - E) | (E * E)<br>
B ::= true | false | (!B) | (B & B) | (B || B) | (E < E)<br>
| (E > E) | (E <= E) | (E >= E) | (E == E) | (E != E)<br>
C ::= x = E | C; C | if B {C} else {C} | while B {C}
</div>
Where E is an expression, B is a boolean expression, and C is a command.
<h4>Details</h4>
The syntax of the program, to be accepted by the program checker, must follow
a generic C syntax. One of the most notable differences is that compound expressions
must be written between parentheses. This means that mathematical operations like multiplication
must be written like the following: ((x * y) + 3) and not
x * y + 3. Another fairly large difference is that the checker does
not support function definitions.<br><br>
A program can have three types of statements: assignment statements, if statements, and
while statements.<br><br>
Assignment statements are of the form:
<pre><variable> = <expression></pre>
Variables need not be declared beforehand.
A variable can contain letters, digits, and underscores, but cannot start with a digit.
Expressions are mathematical expressions. They can be another variable, a number, or
an expression of the form:
<pre>(<expression> <op> <expression>)</pre>
Where op is one of +, -, or *. An expression can also be negated by prepending it
with a dash (-) and surrounding both with parentheses (for example, (-<expression>)).<br><br>
If statements are of the form:
<pre>if <boolean> {<br>...<br>} else {<br>...<br>}</pre>
Within the curly braces there must be at least one statement. The boolean is a boolean
expression which can simply be the values true or false, a comparison of boolean expressions
(where the operators are || and &), the negation of a boolean expression (in the form (!<boolean>))
by prepending it with !, or a comparison between mathematical expressions using <, >,
<=, >=, ==, or !=.
Finally, while statements are of the form:
<pre>while <boolean> {<br>...<br>}</pre>
The boolean expression follows the same syntactical rules as for the boolean expression in an
if statement. There must be at least one statement within the curly braces.
</div>
</div>
</div>
<div class="panel panel-danger panel-instruction">
<div class="panel-heading pointer collapsed" role="tab" id="headingInvVar"
data-toggle="collapse" data-parent="#instructionGroup"
aria-expanded="true" aria-controls="collapseInvVar" href="#collapseInvVar">
<div class="panel-title">
<span class="glyphicon collapse-instruction"></span>
Invariants and Variants
</div>
</div>
<div id="collapseInvVar" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingInvVar">
<div class="panel-body">
Invariants and variants are only necessary when writing while loops. Without a while loop
there will be no option to add invariants or variants. If the program contains one
or many loops, then a box will appear containing the necessary amount of inputs for
the invariants and variants. The order in which the invariants and variants should be
filled out follows the textual order of the while loops. Nesting loops has no effect.
For example:
<pre>while (x < 10) {
while (y < 10) {
z = (z + 1);
y = (y + 1);
}
x = (x + 1);
}
</pre>
The first invariant and variant would correspond to the <strong>while (x < 10)</strong>
and the second would correspond to the <strong>while (y < 10)</strong>.
<h3>Invariants</h3>
Invariants are propositional logic formulas that are always true during the execution
of a while loop. They are used to help generate the formulas needed to prove the validity
of the program in terms of partial correctness. Like pre- and postconditions, the user may
specify anything as an invariant, but should follow the table of symbols in
<strong>Preconditions and Postconditions</strong> to make full use of the program checker's
ability to recognize symbols and properly format their output.
<h3>Variants</h3>
Variants are expressions that are constantly changing during the execution
of a while loop such that the value of the expression eventually reaches 0. They are used to
help generate the formulas needed to prove the validity
of the program in terms of total correctness. Like pre- and postconditions, the user may specify
anything as a variant, but should follow the table of symbols in <strong>Preconditions and
Postconditions</strong> to make full use of the program checker's ability to recognize symbols
and properly format their output.<br><br>
An element that appears in variants that do not appear in invariants is the <strong>init</strong>
logic variable. It represents some value to which a program loop variable must be equal.
</div>
</div>
</div>
<div class="panel panel-danger panel-instruction">
<div class="panel-heading pointer collapsed" role="tab" id="headingOutput"
data-toggle="collapse" data-parent="#instructionGroup"
aria-expanded="true" aria-controls="collapseOutput" href="#collapseOutput">
<div class="panel-title">
<span class="glyphicon collapse-instruction"></span>
Proofs
</div>
</div>
<div id="collapseOutput" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingOutput">
<div class="panel-body">
Proofs appear in their own box once the program has been submitted and processed by the
program checker. The formulas that appear in this box are propositional logic formulas
that need to be proven so that the validity of the program can be proven. This can
be done by hand or by using one of many theorem provers available. The formulas are divided
into two sections:
<h3>Partial Correctness Proofs</h3>
If the formulas in this section can be proven, then one can prove the validity of the program
in terms of partial correctness. This means that termination of the program <strong>is not</strong>
taken into account in these proofs.
<h3>Total Correctness Proofs</h3>
If the formulas in this section can be proven, then one can prove the validity of the program
in terms of total correctness. This means that termination of the program <strong>is</strong>
taken into account in these proofs.
</div>
</div>
</div>
<div class="panel panel-danger panel-instruction">
<div class="panel-heading pointer collapsed" role="tab" id="headingExample"
data-toggle="collapse" data-parent="#instructionGroup"
aria-expanded="true" aria-controls="collapseExample" href="#collapseExample">
<div class="panel-title" href="#arrow">
<span id="arrow" class="glyphicon collapse-instruction"></span>
Example
</div>
</div>
<div id="collapseExample" class="panel-collapse collapse" role="tabpanel" aria-labelledby="headingExample">
<div class="panel-body">
Here is a small example of the workflow of the program checker application.
<h3>Program</h3>
Use the following program as an example:
<pre>
y = 0;
x = 0;
while (x != w) {
x = (x + 1);
y = (y + z);
}
</pre>
Insert the program into the program input box.
<img class="screenshot" src="static/img/program.png"
alt="Program inserted in the program text area"></img>
Next, use the following as the precondition:
<pre>w >= 0</pre>
and put it into the precondition box:
<img class="screenshot" src="static/img/precondition.png"
alt="Precondition inserted into the precondition input box"></img>
Use the following as the postcondition:
<pre>y = w * z</pre>
and put it into the postcondition box:
<img class="screenshot" src="static/img/postcondition.png"
alt="Postcondition inserted into the postcondition input box"></img>
Following that, use <pre>y = x * z</pre> as invariant 1,
and use <pre>w - x</pre> as variant 1.
<img class="screenshot" src="static/img/invVar.png"
alt="Invariant 1 and variant 1 inserted into their respective inputs"></img>
Finally, click the submit button and look at the results in the <strong>Proofs</strong> box.
It should look like this:
<img class="screenshot" src="static/img/proofs.png"
alt="Resulting proofs from running the example"></img>
So to prove the validity of the program, one must prove that each of the formulas hold,
either for partial or total correctness.
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>