From f9fb3ef40b56bedf29839daa3cfe9153ae94d932 Mon Sep 17 00:00:00 2001 From: Tony Knapp <5892063+texastony@users.noreply.github.com> Date: Thu, 7 Nov 2024 12:04:10 -0800 Subject: [PATCH] chore(STD-Dafny): HasSubString (#952) * chore(STD-Dafny): HasSubString --- StandardLibrary/src/Sequence.dfy | 42 +++++++++++++++++++++++++++++ StandardLibrary/src/String.dfy | 40 ++++++++++++++++++++++++++- StandardLibrary/src/UInt.dfy | 1 + StandardLibrary/test/TestString.dfy | 35 ++++++++++++++++++++++++ 4 files changed, 117 insertions(+), 1 deletion(-) create mode 100644 StandardLibrary/src/Sequence.dfy create mode 100644 StandardLibrary/test/TestString.dfy diff --git a/StandardLibrary/src/Sequence.dfy b/StandardLibrary/src/Sequence.dfy new file mode 100644 index 000000000..2f87dd309 --- /dev/null +++ b/StandardLibrary/src/Sequence.dfy @@ -0,0 +1,42 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "UInt.dfy" + +module StandardLibrary.Sequence { + // export provides SequenceEqual, StandardLibrary + import opened UInt + + predicate method SequenceEqualNat(seq1: seq, seq2: seq, start1: nat, start2: nat, size: nat) : (ret : bool) + requires start1 + size <= |seq1| + requires start2 + size <= |seq2| + ensures ret ==> seq1[start1..start1 + size] == seq2[start2..start2 + size] + { + if |seq1| > UINT64_MAX_LIMIT || |seq2| > UINT64_MAX_LIMIT then + // This line of code will never be executed, but is included for correctness + seq1[start1..start1 + size] == seq2[start2..start2 + size] + else + SequenceEqual(seq1, seq2, start1 as uint64, start2 as uint64, size as uint64) + } + + predicate SequenceEqual(seq1: seq64, seq2: seq64, start1: uint64, start2: uint64, size: uint64) : (ret : bool) + requires start1 as nat + size as nat <= |seq1| + requires start2 as nat + size as nat <= |seq2| + ensures ret <==> seq1[start1..start1 + size] == seq2[start2..start2 + size] + { + seq1[start1..start1 + size] == seq2[start2..start2 + size] + } by method { + var j := start2 as uint64; + for i := start1 as uint64 to (start1 + size) as uint64 + invariant j == i - start1 + start2 + invariant forall k : uint64 | start1 <= k < i :: seq1[k] == seq2[k - start1 + start2] + { + if seq1[i] != seq2[j] { + return false; + } + j := j + 1; + } + return true; + } + +} diff --git a/StandardLibrary/src/String.dfy b/StandardLibrary/src/String.dfy index f7a384d0a..2c34ec532 100644 --- a/StandardLibrary/src/String.dfy +++ b/StandardLibrary/src/String.dfy @@ -1,8 +1,13 @@ // Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. // SPDX-License-Identifier: Apache-2.0 +include "../../libraries/src/Wrappers.dfy" +include "Sequence.dfy" module StandardLibrary.String { - export provides Int2String, Base10Int2String + import Wrappers + import opened UInt + import opened Sequence + export provides Int2String, Base10Int2String, HasSubString, Wrappers, UInt const Base10: seq := ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9'] @@ -48,4 +53,37 @@ module StandardLibrary.String { { Int2String(n, Base10) } + + /* Returns the index of a substring or None, if the substring is not in the string */ + method HasSubString(haystack: string, needle: string) + returns (o: Wrappers.Option) + + ensures o.Some? ==> + && o.value <= |haystack| - |needle| && haystack[o.value..(o.value + |needle|)] == needle + && (forall i | 0 <= i < o.value :: haystack[i..][..|needle|] != needle) + + ensures |haystack| < |needle| || |haystack| > (UINT64_MAX_LIMIT-1) ==> o.None? + + ensures o.None? && |needle| <= |haystack| && |haystack| <= (UINT64_MAX_LIMIT-1) ==> + (forall i | 0 <= i <= (|haystack|-|needle|) :: haystack[i..][..|needle|] != needle) + { + if |haystack| < |needle| { + return Wrappers.None; + } + + // `-1` is needed because of how `limit` is calculated below + expect |haystack| <= (UINT64_MAX_LIMIT-1); + + var size : uint64 := |needle| as uint64; + var limit: uint64 := |haystack| as uint64 - size + 1; + + for index := 0 to limit + invariant forall i | 0 <= i < index :: haystack[i..][..size] != needle + { + if SequenceEqual(seq1 := haystack, seq2 := needle, start1 := index, start2 := 0, size := size) { + return Wrappers.Some(index as nat); + } + } + return Wrappers.None; + } } diff --git a/StandardLibrary/src/UInt.dfy b/StandardLibrary/src/UInt.dfy index 7bd825eb7..2f9daf062 100644 --- a/StandardLibrary/src/UInt.dfy +++ b/StandardLibrary/src/UInt.dfy @@ -16,6 +16,7 @@ module StandardLibrary.UInt { const UINT64_LIMIT := BoundedInts.UINT64_MAX as int + 1 const INT32_MAX_LIMIT := BoundedInts.INT32_MAX as int const INT64_MAX_LIMIT := BoundedInts.INT64_MAX as int + const UINT64_MAX_LIMIT := BoundedInts.UINT64_MAX as int predicate method UInt8Less(a: uint8, b: uint8) { a < b } diff --git a/StandardLibrary/test/TestString.dfy b/StandardLibrary/test/TestString.dfy new file mode 100644 index 000000000..8833c3198 --- /dev/null +++ b/StandardLibrary/test/TestString.dfy @@ -0,0 +1,35 @@ +// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved. +// SPDX-License-Identifier: Apache-2.0 + +include "../src/StandardLibrary.dfy" +include "../src/String.dfy" +include "../../libraries/src/Wrappers.dfy" + +module TestStrings { + import StandardLibrary.String + import opened Wrappers + + method {:test} TestHasSubStringPositive() + { + var actual := String.HasSubString("Koda is a Dog.", "Koda"); + expect actual == Some(0), "'Koda' is in 'Koda is a Dog.' at index 0, but HasSubString does not think so"; + actual := String.HasSubString("Koda is a Dog.", "Koda is a Dog."); + expect actual == Some(0), "'Koda is a Dog.' is in 'Koda is a Dog.' at index 0, but HasSubString does not think so"; + actual := String.HasSubString("Koda is a Dog.", "Dog."); + expect actual == Some(10), "'Dog.' is in 'Koda is a Dog.' at index 10, but HasSubString does not think so"; + actual := String.HasSubString("Koda is a Dog.", "."); + expect actual == Some(13), "'.' is in 'Koda is a Dog.' at index 13, but HasSubString does not think so"; + actual := String.HasSubString("Koda is a Dog.", ""); + expect actual == Some(0), "The empty string is in 'Koda is a Dog.' at index 0, but HasSubString does not think so"; + } + + method {:test} TestHasSubStringNegative() + { + var actual := String.HasSubString("Robbie is a Dog.", "Koda"); + expect actual == None, "'Robbie is a Dog.' does not contain Koda"; + actual := String.HasSubString("\t", " "); + expect actual == None, "A tab is not a space"; + actual := String.HasSubString("large", "larger"); + expect actual == None, "Needle larger than haystack"; + } +}