george: User Manual

[ Introduction ] [ File Structure ] [ #check PROP ] [ #check PRED ] [ #check PREDTYPES ] [ #check TP ]
[ #check ND ] [ #check ST ] [ Arithmetic ] [ Sets ] [ #check Z ] [ #check PC ]
[ Contributions by Students ] [ Credits ] Keywords ]

Structure of Input

The input to george is a text file structured into sections. For example:

#u nday
#a 01


#q 01a

#check PROP

...

#check ND

...

// This is a comment.

// ...

#q 01b

...

#q 02

...

A ``#'' at the beginning of a line is a directive to the tool. george understands the following directives:

Directive	Meaning
u username	States your username "username'' If working in a group of two (which is allowed in some terms but not all terms), please place the second user name after the first on the same line, as in #u user1 user2
a id	States the assignment name/number
q id	Begins a section for the question id
#check x	Tells george that the lines that follow (until the next directive) are a soln of the form of method "x''. george will invoke the correctness checks that it has for this method. The methods george currently supports are: PROP The solution is a single formula in propositional logic. PRED The solution is a single formula in predicate logic. TP The solution is a proof in transformational proof. ND The solution is a proof in natural deduction. ST The solution is a proof in semantic tableaux. Z The solution is a Z specification PC The solution is an annotated program.

Comments

A ``//'' at the beginning of a line anywhere in the file is comment that ends at the end of the line.

Multi-line comments can be enclosed within ``/* ... */''.

Comment lines can be used to answer questions whose answer does not consist entirely of a formula or proof, as well as, for any additional information you wish to pass along to the TA who will mark your assignment. Comments are not parsed by george.

Questions

A question/section may have multiple parts to it (e.g., Q01b may require a propositional logic formula and a natural deduction proof. And a question may require you to use multiple #check directives.

Note: For SE212, each assignment question is to be placed in its own text file to be submitted to MarkUs (e.g., all parts of Q01 in one file, all parts of Q02 in one file, etc.), which has already been set up in the skeleton solution files that you receive for the assignment. You can use these files each individually in george.

The following sections explain the correctness checks that carries out for each method.