/usr/share/spark/checker/rules/SEQ.RUL is in spark 2012.0.deb-11.
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 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 | % -----------------------------------------------------------------------------
% (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 :-
%
% seqlen : properties of the length of sequence function
% append : properties of the append operator
% first : properties of the sequence function first
% last : properties of the sequence function last
% nonfirst : properties of the sequence function nonfirst
% nonlast : properties of the sequence function nonlast
% seq : equality properties of sequences
%-------------------------------------------------------------------------------
% MODEL DECLARATIONS FOR THIS FILE :-
%
% rule_family seqlen:
% X >= Y requires [ X:i, Y:i ] &
% X > Y requires [ X:i, Y:i ] &
% length(X) requires [ X:any ] &
% X + Y requires [ X:i, Y:i ] &
% X - Y requires [ X:i, Y:i ].
%
% rule_family append:
% X @ Y requires [ X:any, Y:any ].
%
% rule_family first:
% first(X) requires [ X:any ].
%
% rule_family last:
% last(X) requires [ X:any ].
%
% rule_family nonfirst:
% nonfirst(X) requires [ X:any ] &
% X @ Y requires [ X:any, Y:any ].
%
% rule_family nonlast:
% nonlast(X) requires [ X:any ] &
% [X|Y] requires [ X:any, Y:any ] &
% X @ Y requires [ X:any, Y:any ].
%
% rule_family seq:
% X <-> Y requires [ X:any, Y:any ] &
% X = Y requires [ X:any, Y:any ].
%-------------------------------------------------------------------------------
/*** Sequence length rules ***/
seqlen(1): length(S)>=0 may_be_deduced.
seqlen(2): length([H|T])>0 may_be_deduced.
seqlen(3): length([H|T])>=1 may_be_deduced.
seqlen(4): length([]) may_be_replaced_by 0.
seqlen(5): length([H|T]) may_be_replaced_by N if
[ goal(length([H|T],N)) ].
seqlen(6): length(S @ T) & length(S)+length(T) are_interchangeable.
seqlen(7): length(S) & length(nonlast(S))+1 are_interchangeable if
[ S<>[] ].
seqlen(8): length(S) & length(nonlast(S))+1 are_interchangeable if
[ length(S)>=1 ].
seqlen(9): length(S)-1 & length(nonlast(S)) are_interchangeable if
[ S<>[] ].
seqlen(10): length(S)-1 & length(nonlast(S)) are_interchangeable if
[ length(S)>=1 ].
seqlen(11): length(S) & length(nonfirst(S))+1 are_interchangeable if
[ S<>[] ].
seqlen(12): length(S) & length(nonfirst(S))+1 are_interchangeable if
[ length(S)>=1 ].
seqlen(13): length(S)-1 & length(nonfirst(S)) are_interchangeable if
[ S<>[] ].
seqlen(14): length(S)-1 & length(nonfirst(S)) are_interchangeable if
[ length(S)>=1 ].
/*** Append rules ***/
append(1): ([] @ L) may_be_replaced_by L.
append(2): (L @ []) may_be_replaced_by L.
append(3): ([H1|T1] @ [H2|T2]) may_be_replaced_by L if
[ goal(append([H1|T1],[H2|T2],L)) ].
append(4): ([first(S)] @ nonfirst(S)) may_be_replaced_by S if [ S<>[] ].
append(5): (nonlast(S) @ [last(S)]) may_be_replaced_by S if [ S<>[] ].
append(6): ((X @ Y) @ Z) & (X @ (Y @ Z)) are_interchangeable.
/*** First rules ***/
first(1): first([H|T]) may_be_replaced_by H.
first(2): first([H|T] @ Y) may_be_replaced_by H.
first(3): first(X @ Y) & first(X) are_interchangeable if [ X<>[] ].
/*** Last rules ***/
last(1): last([H]) may_be_replaced_by H.
last(2): last(X @ [H|T]) may_be_replaced_by last([H|T]).
last(3): last([H|T]) & last(T) are_interchangeable if [ T<>[] ].
last(4): last(X @ Y) & last(Y) are_interchangeable if [ Y<>[] ].
/*** Nonfirst rules ***/
nonfirst(1): nonfirst([H|T]) may_be_replaced_by T.
nonfirst(2): nonfirst(T) may_be_replaced_by [] if [ length(T)=1 ].
nonfirst(3): nonfirst(X @ Y) & nonfirst(X) @ Y are_interchangeable if
[ X<>[] ].
nonfirst(4): nonfirst([H|T] @ Y) may_be_replaced_by T @ Y.
/*** Nonlast rules ***/
nonlast(1): nonlast([H]) may_be_replaced_by [].
nonlast(2): nonlast(T) may_be_replaced_by [] if [ length(T)=1 ].
nonlast(3): nonlast([H|T]) & [H|T1] are_interchangeable if
[ nonlast(T)=T1 ].
nonlast(4): nonlast(X @ Y) & X @ nonlast(Y) are_interchangeable if
[ Y<>[] ].
nonlast(5): nonlast(X @ [H]) may_be_replaced_by X.
/*** Sequence Equality rules ***/
seq(1): X = Y <-> ((first(X)=first(Y) and nonfirst(X)=nonfirst(Y))
or (X=[] and Y=[]))
may_be_deduced.
seq(2): X = Y may_be_deduced_from
[ first(X)=first(Y), nonfirst(X)=nonfirst(Y) ].
seq(3): X = Y <-> ((nonlast(X)=nonlast(Y) and last(X)=last(Y))
or (X=[] and Y=[]))
may_be_deduced.
seq(4): X = Y may_be_deduced_from
[ nonlast(X)=nonlast(Y), last(X)=last(Y) ].
|