From 80a4e61b4429dbc4a4ae60c57616a4af700a3fe5 Mon Sep 17 00:00:00 2001 From: Jhon Tabio Date: Tue, 26 Mar 2024 19:04:54 -0400 Subject: [PATCH] String method 'contains' had issues with not being pure, although it is a pure method. Talked with Leavens and came to this solution --- specs/java/lang/String.jml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/specs/java/lang/String.jml b/specs/java/lang/String.jml index 3011aeb..0af99f3 100644 --- a/specs/java/lang/String.jml +++ b/specs/java/lang/String.jml @@ -480,6 +480,13 @@ public final class String @*/ public /*@ pure @*/ boolean contentEquals(StringBuffer sb); + /*@ public normal_behavior + @ ensures \result == (\exists int i; 0 <= i && i < this.length(); + @ (\forall int j; 0 <= j && j < s.length(); + @ this.charAt(i+j) == s.charAt(i+j))); + @*/ + public /*@ pure @*/ boolean contains(CharSequence s); + /*@ public normal_behavior @ ensures \result <==> (c1 == c2) @ || (Character.toUpperCase(c1)