Future directions
From Automated Assistance for Formal Reasoning
Contents |
[edit] Specific Projects
Descriptions and requirements for the three aartifact project types from the Spring 2011 iteration of the Boston University course CS 511 can be found in the following articles:
- #5: Projects: Client-side Parsing and Verification
- #6: Projects: Client-side Transitive Closure Computation
- #7: Projects: Logical Validation in a Scripting Language
Links to the pages for each project type can also be found on the left-hand sidebar of this website.
NOTE: These articles will be updated and extended over time. However, once a requirement is listed in an article, it will never change and will not be removed.
[edit] Specific Projects: Original High-level Overviews
Below are proposals for three projects that could be completed in about one semester. The fourth project could be an extra feature added to one of the three base projects if there is time.
[edit] 1. Client-side Parsing and Verification
Implement a client-side logical verification tool to complement and mirror the server-side validation capabilities of the AARTIFACT system.
This project involves the implementation of:
- a recursive descent parser for logical expressions;
- a collection of one or more validation procedures;
- error reporting capabilities.
The parser should be able to handle the subset of the concrete syntax that includes predicates, disjunction, conjunction, negation, universal quantifiers, and existential quantifiers. Assistance in implementing a parser will be provided in the form of examples and/or skeleton code.
The collection of validation procedures should include a procedure that checks that syntax is valid and that all variables are bound. The collection should also include a procedure that verifies that a proposition is true according to propositional logic. Other validation procedures (e.g. FOL or a subset thereof) can be proposed and implemented.
The tool should be implemented using JavaScript, should be efficient and well-documented, and should be compatible with most browsers. Related tools such as the Google Web Toolkit or jQuery may be useful for implementing the entire tool or components thereof. Those working on this project may also consider adding the "Flexible Interface for Proof Sketching" feature described further below.
[edit] 2. Client-side Transitive Closure Computation
Implement using a client-side scripting language (i.e. JavaScript) an efficient algorithm for performing transitive closure computations for predicates that govern a set of logical expressions.
A fixed collection of logical implications will be provided to the algorithm in a specified, standardized format. The implications will be roughly of the following form, where P, Q, and R are predicates.
for all x1, x2, x3. P(x1,x2) and Q(x2,x3) => R(x1,x3)
A hypergraph is an abstract concept that can be used to represent how a collection of predicates applies to a collection of expressions. For example, suppose the predicate * is less than * applies to the expressions 1 and 2 (because 1 is less than 2 is a true expression). This can be represented using a graph in which 1 and 2 are nodes and * is less than * is a labelled edge. If we allow edges to have zero or more nodes (since the predicates they represent can have zero or more arguments), this becomes a hypergraph.
The algorithm should represent a collection of predicates and how they apply to a collection of expressions by maintaining a data structure similar to a hypergraph. It should be able to compute the transitive closure of any instance of a hypergraph with respect to the fixed collection of logical implications.
The focus of this project is a correct (logically consistent) but also efficient implementation of the hypergraph data structure and closure algorithm. Existing techniques from related literature on computing congruence closures can be consulted. It should be possible to integrate this algorithm with reasonably little effort with any tools produced by the first project ("Client-side Parsing and Verification") described above.
[edit] 3. Logical Validation in a Scripting Language
Implement a Python library that allows users to assume and assert logical properties that values and expressions (numbers, arrays, dictionaries/finite maps) in their programs might have. This library should mirror the verification capabilities of the AARTIFACT system. An advanced implementation could integrate these capabilities with the native control flow and logical constructs found in Python (e.g. procedure calls and if statements).
By importing the library developed in this project, users should be able to insert assumptions and assertions into their programs that use a logical syntax and that will be checked at run-time. For example, the following Python program should generate no run-time errors because the asserted fact is true.
import pyaartifact xs = [1,3,5] assert(dir(), "for x in xs: x is odd")
The components of this library can include:
- a parser for logical expressions;
- an interpreter that can evaluate logical expressions (it may be useful to employ the Python
eval()anddir()functions to handle syntax such as that presented above); - a logical validation algorithm for expressions.
The following component could be added if time and resources permit:
- a global data structure for keeping track of which predicates apply to which expressions (such as the hypergraph discussed in the "Client-side Transitive Closure Computation" project description above);
It is acceptable to start the project by first implementing a basic parser and validation procedure for logical expressions using Python. Use of a library such as PyLog is acceptable as long as it is used in a way that does not introduce logical inconsistencies.
Subsequent revisions can add more features, such as the inclusion of Python variables and constants within logical expressions.
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] *Extra. Flexible Interface for Proof Sketching
This project is more of a feature that might be implemented as part of one of the other projects.
Using JavaScript or related tools, implement a graphical user interface for sketching proofs that works like a flexible notepad.
Users should be able to type text anywhere on the page, and should be able to move any pieces or collections of text around as they see fit. At any given moment, an algorithm should make its best effort to parse and validate the text, or parts of the text, that is found on the screen (the algorithm may assume that text is written top-to-bottom, left-to-right).
Because users should be able to save and store their proof sketch (e.g. in a database), any such tool should be able to convert a sketch from and to an ASCII or binary representation.
[edit] General Directions
[edit] Interface
Further improvements to the interface can revolve around better integration of components and a more interactive user experience. Users should get feedback about proper syntax, selection of syntactic idioms, and even validity of statements as they are typing formal arguments.
Other improvements to the interface include the integration of systems for sketching formal structures. For example, it should be possible to sketch diagrams of structures such as graphs, and to then include these graphs within the dynamic context so that assertions can be made about their properties.
[edit] Efficient operation of validation procedures
The dynamic context uses a large amount of memory, and computing the closure procedure can take a substantial amount of time. It is necessary to make the implementation of the dynamic context more space-efficient. It is also necessary to develop heuristic techniques for predicting and avoiding worst-case formal arguments that cause superlinear growth in the size of the dynamic context. Currently, worst-case scenarios such as the following cause quadratic growth:
Assert $14*x = x+x+x+x+x+x+x+x+x+x+x+x+x+x$.
[edit] Infrastructure and distribution
This system can be deployed as a web application within a classroom or work environment if it is hosted on the cloud. One possible approach is to set up an environment such as this instance of MediaWiki along with a collection of validation servers. An infrastructure would need to be set up to distribute the load of validation requests across these servers.
This system can also be deployed by clients in their own environment. Currently, this requires installation of the Haskell Platform, and use of a command-line interface. Neither of these are ideal. It is preferable to make available a single package to users that contains both the system and any necessary supporting environment. This may require recoding (or compiling) the entire system in a different language or on a different platform.
A significant portion of the system's error detection and validation capabilities can be implemented as a client-side browser application. Such an effort would involve implementation of a parser and validation procedure using JavaScript/AJAX/jQuery/GWT. This could then be integrated into the existing client-side application.
[edit] Integration with existing systems
Because the primary purpose of the system is to act as a user-friendly interface for verification capabilities, it is natural to implement translations that transform the inferences performed by the system's validation procedure into proofs that can be verified with some other existing verification system. This would require the creation of a back-end component that generates formal proofs that can be verified by Mizar, an instantiation of Isabelle, or even Coq. It would also be necessary to assemble a static context of propositions that corresponds to the target system. Such an exercise would enhance our system's usefulness by allowing users to validate their arguments with respect to a well-established system. It would also provide a way to further evaluate the usability benefits provided by our system. It would also potentially foster more interaction with the formal verification community.
[edit] Applications
The approaches adopted in the development of this system can be applied more widely. The system's static context can be instantiated with concepts and propositions from a particular domain. It would then be possible evaluate whether there are any benefits within that context of the immediate feedback and lightweight validation provided by our system.
For example, it should be possible to assemble a static context for particular programming languages. This context might include code templates corresponding to particular common practices or strategies, and propositions that deal with high-level characteristics of user programs. These characteristics may include termination, unused variables, dead code, and others studied in the programming language design and optimization literature. This effort could be further bolstered by developing a separate parser that can accommodate the syntax of the programming language being considered. Such a variant of this system would overlap in motivation and approach to related work [1,2,3].
As another example, it should be possible to assemble a static context of concepts and facts about a family of constraints used within a particular discipline, such as control theory.
[edit] References
[1] Sangmok Han, David R. Wallace, and Robert C. Miller. Code completion from abbreviated input, 2009.
[2] Greg Little and Robert C. Miller. Keyword programming in java, March 2009.
[3] Greg Little, Robert C. Miller, Victoria Chou, Michael Bernstein, Tessa Lau, and Allen Cypher. Sloppy Programming, 2009.