Projects: Logical Validation in a Scripting Language
From Accessible Integrated Formal Reasoning Environments
This article describes the "Logical Validation in a Scripting Language" aartifact project for the Spring 2011 iteration of the Boston University course CS 511. A high-level outline for what your project report should contain can be found here.
NOTE: This article will be updated and extended over time. However, once a requirement is listed in this article, it will never change and will not be removed.
Contents |
[edit] Requirement #1: Propositional Logic
Define Python data structures and functions that can be used to parse and evaluate propositional logic formulas written using the following syntax:
<word> ::= a-zA-Z
<formula> ::= [<word> <word> ... <word>]
| <formula> and <formula>
| <formula> or <formula>
| <formula> implies <formula>
| not <formula>
| { <formula> }
Any sequence of one or more words (each word consisting of characters a-zA-Z) separated by spaces and surrounded by square brackets [...] represents a predicate. Formulas are built up by combining these predicates using the four logical operators. Braces {...} can be used to group formulas. This concrete syntax allows users to write logical formulas such as the following:
[the ground is wet] implies {[it is raining] or [it rained]}
There must exist a function validate() that accepts formulas written using the above syntax and returns True or False as appropriate.
[edit] Details about Parsing
There exists an extensive collection of Python parsing modules. Some, such as PLY, are fairly straightforward to use (example).
[edit] Details about Evaluation
The validation algorithm should correctly determine whether a propositional logic formula represented by the abstract syntax is true or false. In the absence of a context (or, equivalently, given an empty context), the validation algorithm could simply check whether a formula is a tautology. Given a context (contexts are described further below) (Q1 and ... and Qn) and a formula F, it should determine whether ((Q1 and ... and Qn) implies F) is a tautology.
You may want to explore existing logical validation libraries such as PyLog. However, if you decide to use an existing library you must understand how it works and be able to justify that you are using it correctly to perform logical validation.
[edit] Requirement #2: Context Implementing Assumptions and Assertions for Run-time Checking
A context is a list of logical formulas that are believed to be true. Logically, it can be represented using a single formula that is a conjunction of many formulas. As a data structure, it can be implemented as a collection of logical formulas and two associated operations: assume (adding a formula to the collection), and assert (checking whether a formula is in the collection).
Define an object that would allow users to insert assertions for run-time checking of logical assertions directly into their Python code. This would allow users to specify preconditions and assign postconditions for blocks of code or functions (as is often done in comments). This provides both a way to sketch, model, and debug code before writing the details, and a way to introduce dynamic run-time checking that may have more useful error messages.
For example, it should be possible for a user to create the following program:
from pyaartifact import Context
aa = Context()
aa.assume("[data is available] implies [can compute result]")
# code to retrieve data goes here
aa.assume("[data is available]")
# insert a run-time assertion before computing
aa.assert("[can compute result]")
#
You may want to work on creating informative error messages that take advantage of the predicates or formulas that may not have been satisfied in an assertion.
[edit] Requirement #3: Terms and First-order Logic
Extend your parser, validation algorithm, and context to support a larger collection of logical formulas.
You are free to define your own syntax for terms, first-order predicates, and so on as necessary.
For first-order logic, you will need to decide what model(s) will be used to determine whether formulas are true. One way to
approach this is to consider what kinds of scopes might be interesting to a programmer and to provide a way for the programmer to
specify a model explicitly. For programming, these would most likely be data types: the boolean space <code>{True, False}, finite rangers of integers, strings up to a certain length, lists up to a certain length, etc. You could allow the programmer to explicitly supply an ad hoc set or list that defines the scope (e.g. only the two values 729 and 184, because those are the only values a programmer may care about).
[edit] Requirement #4: Examples and Use Cases
Once a stable version of the library has been created, at least two simple examples should be constructed illustrating how it can be used to increase confidence in the correctness of an implementation of algorithms. These algorithms should at least perform some basic computation (e.g. factoring, sorting).
[edit] Further Extensions
Beyond fulfilling the listed requirements, you have a lot of freedom in implementing other extensions or components. These may include better error messages and feedback, better text and graphical interfaces, XML or other standards for exporting and importing data (e.g. use MathML 1, 2), and so forth. Do not hesitate to email questions if you are not sure about your idea.