Comprehensive TODO List

[abhabongse]

Translation Into Alloy Program

Language Parser

• [ ] Implement transformer from Lark parsed tree into internal AST

Verification in Alloy

Translation from AST into Alloy program

• [ ] Use node transformer to convert AST into Alloy program

Alloy Verification Interfaces

• [ ] Textual analysis for Alloy programs (to be expanded)
• [ ] Visualization of Alloy counter-examples (to be expanded)

Additional Verification Features

• [ ] Multiple scalar types in databases
• [ ] Total ordering on scalar types with comparison operators
• [ ] Functional dependencies declaration in database schemata
• [ ] Primary keys, candidate keys, unique keys (dependent of functional dependencies)

[abhabongse]

ASDL might be fun, but it is a waste of time. Might use ANTLR instead.

[abhabongse]

Okay, ANTLR is too heavy of a metal; use LARK instead.

[abhabongse]

Commenced on using Lark Parser.