GCL Parser

A simple parser for the GCL language used in the course Program Verification. The parser is written using Happy and Haskell. A Cabal build file is included to build the library.

This parser admits a richer language than the base GCL to also accommodate optional assignments. You can ignore the parts of the parser/syntax that you don't need in your parts of assignments.

Prerequisites

To compile the tool, the following package are required:

• array
• containers
• optparse-applicative
• pretty.

Compilation

To compile the library, run the command > cabal build from your console.

Running/testing from interpreter

After building (see above), you can run:

> cabal repl

This will run ghci (Haskell interpreter) and also load the module GCLParser.Parser. From there you can load other packages using the usual :l <modulename> command.

The file .ghci in the project root contains ghci options that will also be turned on. Currently it only contains:

-XNamedFieldPuns

Usage

The module GCLParser.Parser exports two functions:

parseGCLstring :: String -> ParseResult Program
parseGCLfile :: FilePath -> IO (ParseResult Program)

The first is to parse a GCL program from a string, and the second is to parse from a text file. The parser returns a value of type ParseResult Program, which is a synonym for Either String Program. Such value takes the form of either Left e where e is an error message if the parsing fails, or Right p if the parsing is successful. In the later case, p is a value of type Program which is a datatype used to structurally repfresent a GCL program. See the module GCLParser.GCLDatatype for its definition.

Note that the module GCLParser.Parser is generated by Happy. The source code is src/GCLParser/Parser.y, which is a Happy parser definition. So, if you need to change the parser, you should not edit Parser.hs manually, but instead edit Parser.y.

Other tools

Pretty printing

The module GCLParser.PrettyPrint provides a function to pretty print a value of type Program:

ppProgram2String :: Program -> String

interpreter (running a GCL program)

The module GCLInterpreter provides a function to execute a GCL program, given a starting state.

execProgram :: Program -> State -> Either (String,State) State

Be mindful that this tool is experimental, and is not made for performance. There is also some incompleteness when interpreting the ∀ and ∃ quantifiers. Obviously, we can't actually check such a quantifier over the whole space of integers, so some practical choice was made. See the module in-code documentation.

mutation test

The module MuGCL provides a function that generate mutants of a GCL Program. Given a program P, the function below generates a bunch of so-called mutants. Each is a program P', which is a copy of P, but where it is changed in one place (e.g. some expression "i<n" is mutated to "i<=n").

mutateProgram :: Program -> [(MutationType,Program)]

You can use this mutants to test the completeness of your verification tool (it should be able to kill all the mutants, but see also my note in the documentation of MuGCL).

Supported GCL syntax

See in /docs.

Error message

Unfortunately almost none. But if some of you know how to make Happy produces a more friendly error message, do let me know.

GCL examples and verification benchmark

See in /examples

Z3

• A note on how to install Z3 for your Haskell project.
• Some examples of how to use Z3 from Haskell: in examples/examplesHaskellZ3.

Papers for your Related Work section

Credits

Many thanks to Stefan Koppier for providing the initial implementation of the parser.

Contributors: Stefan Koppier, Wishnu Prasetya