Tools

AguiaJ

AguiaJ is an pedagogical environment for experimenting object-oriented programming in Java. The tool enables users to interactively test object classes by creating and manipulating objects and visualizing the result of such interaction in terms of object state. The notion of encapsulation is metaphorically embodied in the environment, by restricting visibility/access to class/package members. Another innovative aspect of the tool is the capability of being extended with model-view plugins that enable users to visualize certain objects with custom views, enriching user experience and enabling introductory programming exercises to deal only with objects as conceptual descriptions of artifacts that are visualized in the tool.

BICA

Bica is an extension of the Java language that enables the verification of Java programs against a session type specification.
This specification represents the changes in the interface of an object.
In Java, the interface of an object is the set of methods declared in the object's class, with visibility taken into account.
Session type specifications provide a more flexible way to specify changes in the interface of an object.

The session type is included in the source code for a class as a Java annotation.
Types are extended with session type information, and Bica verifies that clients of a class use it as specified by the session type.
Bica is implemented using the Polyglot framework, as an extension of the jl5 language extension. That is, it supports Java 5 source code.

ConGu

ConGu is a tool that supports the checking of Java classes against property-driven algebraic specifications. Checking classes consists in determining, at run-time, whether the classes that are subject to analysis behave as required by the specification. The first version of the tool, available here, reduce the problem to the run-time monitoring of contract annotated classes, which is supported today by several runtime assertion-checking tools. In ConGu 2.0, which is also applicable to generic datatypes implemented by generic Java classes, the run-time monitoring of the implementations is achieved through bytecode instrumentantion and use of assertions. ConGu 2.0 is available in the QUEST plug-in for the Eclipse IDE.

DOL

Dependent Object-oriented Language, or DOL for short, is an object-oriented language featuring mutable objects and dependent types that supports class-based inheritance with subtyping.

While rooted in techniques formulated for dependently-typed functional languages, DOL's type system is able to capture more than just value properties and pure computations. Using a combination of index refinements and method type signatures inspired on Hoare-style pre- and postconditions, it gives programmers the ability to reason about effectful computations.

This is (as far as we know) the first implementation of a type system combining three very different features: dependent types, mutable objects, and inheritance with subtyping. With the assistance of an external SMT solver, the tool can verify certain program invariants at compile time, including the binary search tree property.

MIL

MIL (Multithreaded Intermediate Language) is an assembly language targeted at an abstract multi-processor equipped with a shared main memory. Each processor consists of a series of registers and of a local memory for instructions and for local data. The main memory is divided into a heap and a run pool. The heap stores data and code blocks. Data blocks are represented by tuples and may be local to the processor for its exclusive use, or stored in the heap and shared amongst processors. A code block declares the registers it expects (including the type for each register), the required locks, and an instruction set. The run pool contains suspended threads waiting for a free processor.
Read More +

MOOL

Mool is a mini object-oriented language in a Java-like style with support for concurrency, that allows programmers to specify class usage protocols as types. The specification formalizes (1) the available methods, (2) the tests clients must perform on the values returned by methods, and (3) the existence of aliasing and concurrency restrictions, all of which depend on the object’s state.

Linear and shared objects are handled as a single category, allowing linear objects to evolve into shared ones. The Mool type system verifies that methods are called only when available, and by a single client if so specified in the usage type. Mool builds upon previous works on (Modular) Session Types and Linear Type Systems.
Read More +

ParTypes

ParTypes is a toolchain for validating and synthesising message-based programs for Message Passing Interface (MPI) programs.

The general aim is to enforce program compliance with dependent-type based protocol specifications, enforcing properties such as protocol fidelity and the absence of deadlocks. The toolchain is composed of an Eclipse plug-in, an annotated MPI library, a C annotator, and makes use of the Verifying C Compiler (VCC), the Z3 SMT solver, and the Why3 platform.

A key result is that verification of C+MPI programs is immune to the state-explosion problem, and verification times are independent of input parameters such as the number of processes, contrasting with established methodologies for MPI program verification, e.g., employing model checking and/or symbol execution.

The Eclipse plug-in allows for the writing of protocol specifications, verifies that protocols are well formed (with the help of Z3 for checking dependent type restrictions), and generates protocol representations in VCC and WhyML formats for program verification. The plugin also synthesises C+MPI code programs that are correct-by-construction, also annotated with VCC logic that work as a proof of their correctness.

PESTT

PESTT (PESTT an Educational Testing Tool) is an Eclipse plug-in for learning and designing unit tests for the Java language. Currently, PESTT supports unit tests based on the control and data flow graphs (CFG) of methods. It generates the CFG based on the source code of the method, allows for bidirectional linking between the source code and the generated CFG, generates test requirements, determines test paths, and computes the coverage level statistics. It provides full integration with JUnit and reconstructs run paths of each test method, computing statistics either for each test method or for the complete test set. PESTT distinguishes from other coverage analysis testing tools because it is not just a node and branch coverage analyzer. Among other things, it supports many other “more powerful” coverage criteria, like prime path coverage or all def-use paths coverage, and assists the test engineer in the various tasks of the testing activity.

ProPi

ProPi is a tool to statically verify whether message passing programs are free from deadlocks. The tool takes as input a system specified in the pi-calculus, together with typing annotations that describe the communications in the channels, as well as event annotations so as to capture the overall ordering of the communications. The tool produces as result either a positive answer (the system type checks), in which case the properties of protocol fidelity (system communications follow the typing prescription) and progress (deadlock absence) hold. Otherwise, the system exhibits error information so as to allow to identify what is the problem in the system specification. The tool includes an Eclipse plugin and a standalone command line interface.

SePi

SePi is a concurrent, message-passing programming language based on
the pi-calculus. The language features synchronous, bi-directional
channel-based communication.

Programs use primitives to send and receive messages as well as offer
and select choices. Channel interactions are statically verified against
session types describing the kind and order of messages exchanged, as
well as the number of processes that may share a channel.

In order to facilitate a more precise control of program properties,
SePi includes assume and assert primitives at the process level and
refinements at the type level. Refinements are treated linearly,
allowing a finer, resource-oriented use of predicates: each assumption
made supports exactly one an assertion.