Detecting Liskov substitution principle violation (5th defect type)

[Leosimetti]

This PR contains the following changes:

1. Implementation of the analyzer for the 5th defect type;
2. Corresponding Unit-tests of the functionality;
3. Improvements of the logic extraction mechanism: Closes (3rd type) An error in the long chain of call #35 and Closes (3rd type) An error in the chain of inheritance  #36 ;
4. Refactoring of the analysis package;
5. API for polystat.

Defect description

The definition of the Liskov substitution principle is as follows:

The principle defines that objects of a superclass shall be replaceable with objects of its subclasses without breaking the application.

We focus on one specific constraint that Liskov substitution principle enforces:

A subtype is not substitutable for its super type if it strengthens its operations' preconditions, or weakens its operations' postconditions.

Example of the defect

[] > base
  [self x] > f
    seq > @
      assert (x.less 9)
      x.add 1
[] > derived
  base > @
  [self x] > f
    seq > @
      assert (x.greater 9)
      x.sub 1

In this example, the redefinition of method f in the derived object changes the original input domain of argument x from (-inf, 9) to (9, inf). This is a strengthening of the preconditions on method f, which is a violation of the Liskov substitution principle.

Documentation: https://hackmd.io/@_2BO8tPVRp6UE5c1RTpY-Q/rJZrkGNrc.