From d15eb4439559d64b4ad3ea38bdfe21ae89cee06b Mon Sep 17 00:00:00 2001 From: Pascal Devenoge Date: Fri, 22 Mar 2024 13:15:05 +0000 Subject: [PATCH] Expand tuple equality definition for negative indices and references Tuple equality can be established by ensuring that they have the same length and all elements are themselfs pairwise equal. Currently, the definition of the tuple equality function only consideres quantifying over positive integer indices. Since specifications might want to infer equality by quantifying over equivalent negative indices, and translated forall quantifiers might quantify over references and not integer values, additional equivalent postconditions are added to tuple___eq__() to support these cases. --- src/nagini_translation/resources/tuple.sil | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/src/nagini_translation/resources/tuple.sil b/src/nagini_translation/resources/tuple.sil index 6ba49594..4637b477 100644 --- a/src/nagini_translation/resources/tuple.sil +++ b/src/nagini_translation/resources/tuple.sil @@ -133,6 +133,24 @@ function tuple___eq__(self: Ref, other: Ref): Bool { tuple___getitem__(other, i)} i >= 0 && i < tuple___len__(self) ==> object___eq__(tuple___getitem__(self, i), tuple___getitem__(other, i)))) + ensures result <==> + (tuple___len__(self) == tuple___len__(other) && + (forall i: Int :: { tuple___getitem__(self, i) } + { tuple___getitem__(other, i)} + i <= -1 && i >= -tuple___len__(self) + ==> object___eq__(tuple___getitem__(self, i), tuple___getitem__(other, i)))) + ensures result <==> + (tuple___len__(self) == tuple___len__(other) && + (forall i: Ref :: { tuple___getitem__(self, int___unbox__(i)) } + { tuple___getitem__(other, int___unbox__(i))} + issubtype(typeof(i), int()) && int___unbox__(i) >= 0 && int___unbox__(i) < tuple___len__(self) + ==> object___eq__(tuple___getitem__(self, int___unbox__(i)), tuple___getitem__(other, int___unbox__(i))))) + ensures result <==> + (tuple___len__(self) == tuple___len__(other) && + (forall i: Ref :: { tuple___getitem__(self, int___unbox__(i)) } + { tuple___getitem__(other, int___unbox__(i))} + issubtype(typeof(i), int()) && int___unbox__(i) <= -1 && int___unbox__(i) >= -tuple___len__(self) + ==> object___eq__(tuple___getitem__(self, int___unbox__(i)), tuple___getitem__(other, int___unbox__(i))))) domain tuple_types {