<commit_before>Behavioural Subtype Checker
===========================

Checker developed as a proof of concept for the University of Antwerp. 

Checks if a class is a behavioural subtype of another, i.e. complies with the Liskov Substitution Principle  comparing the contracts of all overriding field and methods and ensuring that they do not impose more restrictive conditions than their superclass equals. It does not guarantee that the contract specified for an element is respected in the code within it.

For the comparison, the [Z3 SMT Solver](http://z3.codeplex.com/), by Microsoft Research, is used.

While there are several tools that provide this functionality at runtime, is yet to be developed one that serves statically for the same purpose. This one diggs into that possibility.

Two kind of annotations are supported:

*     **Requires**: Preconditions for methods.
*     **Invariant**: Constraints that must be preserved inside a code block. 


As stated, this work is only a proof of concept and is not suitable for its use in a verification process.

The contracts must be written in [SMT-Lib](http://www.smtlib.org/) format and only integer values are accepted.<commit_msg>updated readme with a link to the paper<commit_after>Behavioural Subtype Checker
===========================

Checker developed as a proof of concept for the University of Antwerp. 

Checks if a class is a behavioural subtype of another, i.e. complies with the Liskov Substitution Principle  comparing the contracts of all overriding field and methods and ensuring that they do not impose more restrictive conditions than their superclass equals. It does not guarantee that the contract specified for an element is respected in the code within it.

For the comparison, the [Z3 SMT Solver](http://z3.codeplex.com/), by Microsoft Research, is used.

While there are several tools that provide this functionality at runtime, is yet to be developed one that serves statically for the same purpose. This one diggs into that possibility.

Two kind of annotations are supported:

*     **Requires**: Preconditions for methods.
*     **Invariant**: Constraints that must be preserved inside a code block. 


As stated, this work is only a proof of concept and is not suitable for its use in a verification process.

The contracts must be written in [SMT-Lib](http://www.smtlib.org/) format and only integer values are accepted.

More information about the motivation for this work and its usage can be found in the related [paper](https://www.dropbox.com/s/8za9s4388layh10/StaticBehaviouralSubtypingMayorga.pdf).
{'fraction_non_alphanumeric': 0.06854062379668849, 'fraction_numerical': 0.004620716211012707, 'mean_word_length': 4.575107296137339, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 1, 'lorem ipsum': 0, 'www.': 3, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '580186', 'n_tokens_mistral': 646, 'n_tokens_neox': 619, 'n_words': 364}