/usr/share/spark/checker/rules/GENINEQS.RUL is in spark 2012.0.deb-11build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 | % -----------------------------------------------------------------------------
% (C) Altran Praxis Limited
% -----------------------------------------------------------------------------
%
% The SPARK toolset is free software; you can redistribute it and/or modify it
% under terms of the GNU General Public License as published by the Free
% Software Foundation; either version 3, or (at your option) any later
% version. The SPARK toolset is distributed in the hope that it will be
% useful, but WITHOUT ANY WARRANTY; without even the implied warranty of
% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
% Public License for more details. You should have received a copy of the GNU
% General Public License distributed with the SPARK toolset; see file
% COPYING3. If not, go to http://www.gnu.org/licenses for a complete copy of
% the license.
%
% =============================================================================
%-------------------------------------------------------------------------------
% RULE FAMILIES CONTAINED HEREIN :-
%
% transitivity : transitivity of relational operators
% strengthen : inequalities strengthening rules
% negation : negation of inequalities rules
%-------------------------------------------------------------------------------
% MODEL DECLARATIONS FOR THIS FILE :-
%
% rule_family transitivity:
% X <= Y requires [ X:ire, Y:ire ] &
% X >= Y requires [ X:ire, Y:ire ] &
% X < Y requires [ X:ire, Y:ire ] &
% X > Y requires [ X:ire, Y:ire ] &
% X = Y requires [ X:any, Y:any ] &
% X <> Y requires [ X:any, Y:any ].
%
% rule_family strengthen:
% X > Y requires [ X:ire, Y:ire ] &
% X < Y requires [ X:ire, Y:ire ] &
% X = Y requires [ X:ire, Y:ire ].
%
% rule_family negation:
% not X requires [ X:any ] &
% X <> Y requires [ X:any, Y:any ] &
% X = Y requires [ X:any, Y:any ] &
% X <= Y requires [ X:ire, Y:ire ] &
% X > Y requires [ X:ire, Y:ire ] &
% X >= Y requires [ X:ire, Y:ire ] &
% X < Y requires [ X:ire, Y:ire ].
%-------------------------------------------------------------------------------
/*** TRANSITIVITY Rules ***/
transitivity(1): I<=K may_be_deduced_from [ I<=J, J<=K ].
transitivity(2): I<=K may_be_deduced_from [ I<=J, J<K ].
transitivity(3): I<=K may_be_deduced_from [ I<=J, J=K ].
transitivity(4): I<=K may_be_deduced_from [ I<J, J<=K ].
transitivity(5): I<=K may_be_deduced_from [ I<J, J<K ].
transitivity(6): I<=K may_be_deduced_from [ I<J, J=K ].
transitivity(7): I<=K may_be_deduced_from [ I=J, J<=K ].
transitivity(8): I<=K may_be_deduced_from [ I=J, J<K ].
transitivity(9): I<=K may_be_deduced_from [ I=J, J=K ].
transitivity(10): K>=I may_be_deduced_from [ I<=J, J<=K ].
transitivity(11): K>=I may_be_deduced_from [ I<=J, J<K ].
transitivity(12): K>=I may_be_deduced_from [ I<=J, J=K ].
transitivity(13): K>=I may_be_deduced_from [ I<J, J<=K ].
transitivity(14): K>=I may_be_deduced_from [ I<J, J<K ].
transitivity(15): K>=I may_be_deduced_from [ I<J, J=K ].
transitivity(16): K>=I may_be_deduced_from [ I=J, J<=K ].
transitivity(17): K>=I may_be_deduced_from [ I=J, J<K ].
transitivity(18): K>=I may_be_deduced_from [ I=J, J=K ].
transitivity(19): I<K may_be_deduced_from [ I<=J, J<K ].
transitivity(20): I<K may_be_deduced_from [ I<J, J<=K ].
transitivity(21): I<K may_be_deduced_from [ I<J, J<K ].
transitivity(22): I<K may_be_deduced_from [ I<J, J=K ].
transitivity(23): I<K may_be_deduced_from [ I=J, J<K ].
transitivity(24): K>I may_be_deduced_from [ I<=J, J<K ].
transitivity(25): K>I may_be_deduced_from [ I<J, J<=K ].
transitivity(26): K>I may_be_deduced_from [ I<J, J<K ].
transitivity(27): K>I may_be_deduced_from [ I<J, J=K ].
transitivity(28): K>I may_be_deduced_from [ I=J, J<K ].
transitivity(29): I=K may_be_deduced_from [ I=J, J=K ].
transitivity(30): I<>K may_be_deduced_from [ I<>J, J=K ].
/*** STRENGTHEN Rules ***/
strengthen(1): I>J may_be_deduced_from [ I>=J, I<>J ].
strengthen(2): J<I may_be_deduced_from [ I>=J, I<>J ].
strengthen(3): I=J may_be_deduced_from [ I>=J, I<=J ].
/*** Rules for manipulation of logical NOT operator ***/
negation(1): not(A=B) & A<>B are_interchangeable.
negation(2): not(A<>B) & A=B are_interchangeable.
negation(3): not(A>B) & A<=B are_interchangeable.
negation(4): not(A<=B) & A>B are_interchangeable.
negation(5): not(A<B) & A>=B are_interchangeable.
negation(6): not(A>=B) & A<B are_interchangeable.
negation(7): not(A=B) & B<>A are_interchangeable.
negation(8): not(A<>B) & B=A are_interchangeable.
negation(9): not(A>B) & B>=A are_interchangeable.
negation(10): not(A<=B) & B<A are_interchangeable.
negation(11): not(A<B) & B<=A are_interchangeable.
negation(12): not(A>=B) & B>A are_interchangeable.
|