Implementation of the analyzer for the 5th defect type;
Corresponding Unit-tests of the functionality;
Improvements of the logic extraction mechanism: Closes #35 and Closes #36 ;
Refactoring of the analysis package;
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.
This PR contains the following changes:
Defect description
The definition of the Liskov substitution principle is as follows:
We focus on one specific constraint that Liskov substitution principle enforces:
Example of the defect
In this example, the redefinition of method
fin thederivedobject changes the original input domain of argumentxfrom (-inf, 9) to (9, inf). This is a strengthening of the preconditions on methodf, which is a violation of the Liskov substitution principle.Documentation: https://hackmd.io/@_2BO8tPVRp6UE5c1RTpY-Q/rJZrkGNrc.