Project Overview

The project is a prototype specialization of the Gillian platform for the Python programming language.

Only basic functionality is implemented and it has some limitations; syntactic sugar is not implemented.

Currently Implemented

• conditional constructs (only two comparison operations: = and <=, and comparison operations are only binary, i.e., you cannot write x < y < z)
• loops - only while
• classes and objects (inheritance not implemented)
• functions
• variable scopes

What Needs to Be Implemented Before the Prototype is Completed

• execution semantics
• assume/assert (the current version became outdated after implementing variable scopes)
• exceptions (there isn't even a basic implementation, risk that a lot of code will need to be changed)
• inheritance (should not be a problem)

Next Steps

After that, examples need to be prepared demonstrating three Gillian capabilities:

• symbolic testing
• verification with separation logic
• checking with bi-abduction

For verification, we can try to implement some algorithm (minimax for tic-tac-toe?) and verify it.