Usinfer
Usinfer is a prototype for behaviour type inference approach that, from a program written in a variation of Mool equipped with assertions, generates the usage types necessary for the program to have its behaviour statically checked by a type system. The tool starts by generating a permissive and nondeterministic state machine representing a typestate, based on the assertions on the code. The tool then translates the generated typestates into usages. In the end, it defines the usage state that each object of the class starts with by using the assertions and the usages obtained in the previous stage. This tool is composed by three algorithms, with the first two adapted from algorithms presented in other works[1,2], and the third one being original.
Download and usage instructions
Download the prototype here
The prototype requires Java 1.7 or higher and the Z3 java bindings. To execute use the following command:
java -jar usinfer.jar <filename> [-typestates]
The prototype will output a .mool file with the program annotated with the generated usages.
The option "-typestates" causes the prototype to print the typestates for each class in the console.
Examples
Below are some examples that can be used to test the prototype:
- FileReader.mools (Output)
- FileReader2.mools (Output)
- Auction.mools (Output)
- Petition.mools (Output)
- Blog.mools (Output)
Source code
Publications
- Cláudio Vasconcelos and António Ravara, From Object-Oriented Code with Assertions to Behavioural Types, OOPS 2017 (pdf)
- Cláudio Vasconcelos, Behavioral Type Inference for Concurrent Object-Oriented Languages, Master thesis, Faculdade de Ciências e Tecnologia of Universidade Nova de Lisboa, 2016 (pdf)
Links
- Syntax for the variation of the Mool language (pdf)
- Master thesis presentation (pdf)
- Detailed execution of the algorithms (pdf)
References
- Guido De Caso et al. “Enabledness-based Program Abstractions for Behavior Validation”. In: ACM Transactions on Software Engineering and Methodology 22.3 (2013), pp. 1–46.
- Peter Collingbourne and Paul H. J. Kelly. “Inference of Session Types From Control Flow”. In: Electronic Notes in Theorectical Computer Science 238.6 (2010), pp. 15–40.