Glossary

The PROSPER Integration Interface The PROSPER Integration Interface (PII) is a specification of communication for verification managed across several components. It consists of a number of layers mostly dealing with communication issues. The top layer, the application support layer, includes operations for manipulating a data type interface data for communication. Anything expressible in higher order logic can be expressed using this datatype. API The API of a component is its signature. It is possible to create an API for a server component. A client component uses this API to call the server's functionality. The Core Proof Engine The Core Proof Engine consists of: An ML implementation of the PII. This includes the ability to connect to plugins across sockets and call functions in a plugin's API. A tagged type for theorems. The primitive inference rules of HOL. The Core Proof Engine has an empty API. HOL98 HOL98 is a highly modular interactive theorem prover. It shares with the Core Proof Engine an implementation of the terms and types of higher order logic, and an implementation of theorems and inference rules. It contains a large amount of other theorem proving support in the form of decision procedures, tactics and proof management capabilities. These can all be added to the Core Proof Engine as extensions that form a custom proof engine. In most cases adding a HOL function to a custom proof engine requires no more than 4 or 5 lines of ML. A Custom Proof Engine A custom proof engine (such as the one shown in Figure 1) consists of the Core Proof Engine extended with some or all of Functions already existing in HOL. PROSPER plugins. User written proof procedures written in ML (possibly using HOL functions or PROSPER plugins). Figure 1: A custom proof engine A custom proof engine has a custom API. Plugin A PROSPER plugin is a verification component that has a PROSPER API. Its functionality can be accessed from a custom proof engine. The Communication Manager The Communication Manager (CM) orchestrates communication between all other PROSPER components. All components must register with the CM before they can communicate. An application (client) is started manually. All other components are started by the CM at the request of clients. The CM can capture the output streams of components and redirect them. The CM also enables a client to interrupt one of its servers using the PII. The PROSPER Database A separate process that contains a copy of the logical theory being used by the proof engine. Client applications and plugins can obtain theory data directly from the database. This is useful if, for example, the proof engine is busy running a proof procedure or waiting for a plugin to produce a result. Proof Engine Modules The PROSPER Toolkit offers a number of modules that can be loaded into custom proof engines. These are a mixture of modules that offer functionality we believe will be commonly needed, examples and specific modules developed for internal projects. Similar modules can be developed by others for custom proof engines. These modules are called proof engine modules. Language-Specific Bindings Most serious applications will want to put a wrapper around an external component's API which makes it appear in a fashion natural to the language of the application. This is called a language-specific binding.

Products

Example Proof Engines The PROSPER Toolkit (see below) comes with three example proof engines and demonstrators for them: A proof engine that has an API database consisting of the primitive rules of inference in the Core Proof Engine. An Interactive Proof proof engine whose API database consists of proof management capabilities based on goaltrees (as they are currently implemented) and a handful of tactics. A BDD proof engine with three functions in its API database, to connect to, disconnect from and call a BDD plugin. Plugins The PROSPER project has developed several plugins, ML bindings for two of which are distributed with the toolkit. The plugins include: Prover Technology's proof tool. This tool and the plugin created from it are distributed separately and require a license to run. The SMV Model Checker. SMV itself is not distributed with the PROSPER Toolkit. A BDD package based on BuDDy which functions as a simple example. IFAD proof engine PROSPER has developed a proof engine suitable for use with IFAD's VDM-SL Toolbox. Hardware Verification Workbench The Hardware Verification Workbench is a new tool underpinned by the PROSPER technology. It contains a proof engine that includes procedures based on the combination of theorem proving and model checking. It also has a natural language interface for entering CTL (or LTL) formulas. The PROSPER Toolkit The PROSPER Toolkit consists of: Implementations of the PII in ML, C, and Java (client-side only). The Core Proof Engine. The Communication Manager (implemented in Java). The PROSPER Database. The example proof engines (except any plugin components they may require). Other examples of modules that can be included in PROSPER APIs. ML bindings for the plugins produced by the PROSPER project. Java demonstration applications for calling the example proof engines.