Skip to content

Commit 74e98c1

Browse files
ajewellamzajewellamz
authored
chore(dafny): add new SearchAndReplaceWhole and friends (#1680)
1 parent 7eafe88 commit 74e98c1

File tree

2 files changed

+177
-13
lines changed

2 files changed

+177
-13
lines changed

‎StandardLibrary/src/String.dfy‎

Lines changed: 106 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,9 @@ module StandardLibrary.String {
88
import opened UInt
99
import opened Sequence
1010
import opened MemoryMath
11-
export provides Int2String, Base10Int2String, HasSubString, Wrappers, UInt, HasSubStringPos, SearchAndReplace, SearchAndReplacePos, SearchAndReplaceAll
11+
export provides Int2String, Base10Int2String, HasSubString, Wrappers, UInt,
12+
HasSubStringPos, SearchAndReplace, SearchAndReplacePos, SearchAndReplaceAll,
13+
SearchAndReplacePosWhole, SearchAndReplaceAllWhole, AlphaNumeric, AlphaNumericUnder
1214

1315
const Base10: seq<char> := ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']
1416

@@ -61,18 +63,8 @@ module StandardLibrary.String {
6163
returns (o : seq<T>)
6264
requires 0 < |old_str|
6365
{
64-
var old_pos := HasSubString(source, old_str);
65-
if old_pos.None? {
66-
return source;
67-
} else {
68-
SequenceIsSafeBecauseItIsInMemory(source);
69-
SequenceIsSafeBecauseItIsInMemory(old_str);
70-
ValueIsSafeBecauseItIsInMemory(old_pos.value);
71-
var pos : uint64 := old_pos.value as uint64;
72-
var source_len : uint64 := |source| as uint64;
73-
var old_str_len : uint64 := |old_str| as uint64;
74-
return source[..pos] + new_str + source[pos+old_str_len..];
75-
}
66+
var x := SearchAndReplacePos(source, old_str, new_str, 0);
67+
return x.0;
7668
}
7769

7870
// Replace first occurrence of old_str after pos in source with new_str and return the result.
@@ -101,6 +93,81 @@ module StandardLibrary.String {
10193
}
10294
}
10395

96+
predicate method BadStart<T(==)>(source : seq<T>, pos : uint64, chars : seq<T>)
97+
requires pos as nat <= |source|
98+
{
99+
if pos == 0 then
100+
false
101+
else
102+
source[pos-1] in chars
103+
}
104+
105+
predicate method BadEnd<T(==)>(source : seq<T>, pos : uint64, match_len : uint64, chars : seq<T>) {
106+
SequenceIsSafeBecauseItIsInMemory(source);
107+
var source_len : uint64 := |source| as uint64;
108+
if Add(pos, match_len) >= source_len then
109+
false
110+
else
111+
source[pos+match_len] in chars
112+
113+
}
114+
predicate method BadMatch<T(==)>(source : seq<T>, pos : uint64, match_len : uint64, chars : seq<T>)
115+
requires pos as nat <= |source|
116+
{
117+
BadStart(source, pos, chars) || BadEnd(source, pos, match_len, chars)
118+
}
119+
120+
const AlphaNumeric : string := "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789"
121+
const AlphaNumericUnder : string := "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789_"
122+
123+
// Replace first occurrence of old_str after pos in source with new_str and return the result.
124+
// If old_str does not exist in source, the source is returned unchanged
125+
// second value in output is None if old_str not found, otherwise it points just after the replaced value
126+
// a match only counts if the character before or after is not in chars
127+
method SearchAndReplacePosWhole<T(==)>(source: seq<T>, old_str: seq<T>, new_str: seq<T>, xpos : uint64, chars : seq<T>)
128+
returns (o : (seq<T>, Option<uint64>))
129+
requires xpos as nat <= |source|
130+
requires 0 < |old_str|
131+
ensures o.1.Some? ==> |o.0| - o.1.value as nat < |source| - xpos as nat
132+
ensures o.1.Some? ==> o.1.value as nat <= |o.0|
133+
{
134+
SequenceIsSafeBecauseItIsInMemory(source);
135+
SequenceIsSafeBecauseItIsInMemory(old_str);
136+
var old_str_len : uint64 := |old_str| as uint64;
137+
var pos : uint64 := xpos;
138+
139+
while pos < |source| as uint64 {
140+
var old_pos := HasSubStringPos(source, old_str, pos);
141+
if old_pos.None? {
142+
return (source, None);
143+
} else if BadMatch(source, old_pos.value, old_str_len, chars) {
144+
pos := old_pos.value + 1;
145+
} else {
146+
SequenceIsSafeBecauseItIsInMemory(source);
147+
SequenceIsSafeBecauseItIsInMemory(new_str);
148+
var source_len : uint64 := |source| as uint64;
149+
var new_str_len : uint64 := |new_str| as uint64;
150+
o := (source[..old_pos.value] + new_str + source[old_pos.value+old_str_len..], Some(Add(old_pos.value, new_str_len)));
151+
assert |o.0| - o.1.value as nat < |source| - pos as nat;
152+
return o;
153+
}
154+
}
155+
return (source, None); // not really needed, but Dafny is dumb
156+
}
157+
158+
// Replace first occurrence of old_str after pos in source with new_str and return the result.
159+
// If old_str does not exist in source, the source is returned unchanged
160+
// second value in output is None if old_str not found, otherwise it points just after the replaced value
161+
// a match only counts if the character before or after is not in chars
162+
method SearchAndReplaceWhole<T(==)>(source: seq<T>, old_str: seq<T>, new_str: seq<T>, chars : seq<T>)
163+
returns (o : (seq<T>, Option<uint64>))
164+
requires 0 < |old_str|
165+
ensures o.1.Some? ==> |o.0| - o.1.value as nat < |source| as nat
166+
ensures o.1.Some? ==> o.1.value as nat <= |o.0|
167+
{
168+
o := SearchAndReplacePosWhole(source, old_str, new_str, 0, chars);
169+
}
170+
104171
// Replace all occurrences of old_str in source with new_str and return the result.
105172
// If old_str does not exist in source, the source is returned unchanged
106173
// safe to use if new_str contains old_str
@@ -125,6 +192,32 @@ module StandardLibrary.String {
125192
}
126193
}
127194

195+
// Replace all occurrences of old_str in source with new_str and return the result.
196+
// If old_str does not exist in source, the source is returned unchanged
197+
// safe to use if new_str contains old_str
198+
// a match only counts if the character before or after is not in chars
199+
method SearchAndReplaceAllWhole<T(==)>(source_in: seq<T>, old_str: seq<T>, new_str: seq<T>, chars : seq<T>)
200+
returns (o : seq<T>)
201+
requires 0 < |old_str|
202+
{
203+
var pos : uint64 := 0;
204+
var source := source_in;
205+
while true
206+
invariant pos as nat <= |source|
207+
decreases |source| - pos as nat
208+
{
209+
var res := SearchAndReplacePosWhole(source, old_str, new_str, pos, chars);
210+
if res.1.None? {
211+
SequenceIsSafeBecauseItIsInMemory(source);
212+
pos := |source| as uint64; // unneeded, but Dafny is dumb
213+
return res.0;
214+
}
215+
source := res.0;
216+
pos := res.1.value;
217+
}
218+
}
219+
220+
128221
/* Returns the index of a substring or None, if the substring is not in the string */
129222
method HasSubString<T(==)>(haystack: seq<T>, needle: seq<T>)
130223
returns (o: Option<nat>)

‎StandardLibrary/test/TestString.dfy‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,27 @@ module TestStrings {
6363
expect actual == "rose_daisy is a rose_daisy is a rose_daisy";
6464
}
6565

66+
method {:test} TestSearchAndReplaceAllWholeEasy()
67+
{
68+
var actual := String.SearchAndReplaceAllWhole("Koda is a Dog.", "Koda", "Robbie", String.AlphaNumericUnder);
69+
expect actual == "Robbie is a Dog.";
70+
actual := String.SearchAndReplaceAllWhole("Koda is a Dog.", "Dog", "good boy", String.AlphaNumericUnder);
71+
expect actual == "Koda is a good boy.";
72+
actual := String.SearchAndReplaceAllWhole("Koda is a Dog.", "Dog.", "good boy!", String.AlphaNumericUnder);
73+
expect actual == "Koda is a good boy!";
74+
actual := String.SearchAndReplaceAllWhole("Koda is a Dog.", "Robbie", "good boy!", String.AlphaNumericUnder);
75+
expect actual == "Koda is a Dog.";
76+
actual := String.SearchAndReplaceAllWhole("Koda is a Dog.", "Koda", "Koda", String.AlphaNumericUnder);
77+
expect actual == "Koda is a Dog.";
78+
79+
actual := String.SearchAndReplaceAllWhole("A rose is a rose is a rose.", "rose", "daisy", String.AlphaNumericUnder);
80+
expect actual == "A daisy is a daisy is a daisy.";
81+
actual := String.SearchAndReplaceAllWhole("rose is a rose is a rose", "rose", "daisy", String.AlphaNumericUnder);
82+
expect actual == "daisy is a daisy is a daisy";
83+
actual := String.SearchAndReplaceAllWhole("rose is a rose is a rose", "rose", "rose_daisy", String.AlphaNumericUnder);
84+
expect actual == "rose_daisy is a rose_daisy is a rose_daisy";
85+
}
86+
6687
method {:test} TestHasSearchAndReplacePos()
6788
{
6889
var actual := String.SearchAndReplacePos("Koda is a Dog.", "Koda", "Robbie", 0);
@@ -91,6 +112,56 @@ module TestStrings {
91112
expect actual == ("Koda is a Dog.", Some(4));
92113
}
93114

115+
// in most cases SearchAndReplacePosWhole is just like SearchAndReplacePos
116+
method {:test} TestHasSearchAndReplacePosWholeEasy()
117+
{
118+
var actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Koda", "Robbie", 0, String.AlphaNumericUnder);
119+
expect actual == ("Robbie is a Dog.", Some(6));
120+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Koda", "Robbie", 1, String.AlphaNumericUnder);
121+
expect actual == ("Koda is a Dog.", None);
122+
123+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Dog", "good boy", 0, String.AlphaNumericUnder);
124+
expect actual == ("Koda is a good boy.", Some(18));
125+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Dog", "good boy", 10, String.AlphaNumericUnder);
126+
expect actual == ("Koda is a good boy.", Some(18));
127+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Dog", "good boy", 11, String.AlphaNumericUnder);
128+
expect actual == ("Koda is a Dog.", None);
129+
130+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Dog.", "good boy!", 0, String.AlphaNumericUnder);
131+
expect actual == ("Koda is a good boy!", Some(19));
132+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Dog.", "good boy!", 10, String.AlphaNumericUnder);
133+
expect actual == ("Koda is a good boy!", Some(19));
134+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Dog.", "good boy!", 11, String.AlphaNumericUnder);
135+
expect actual == ("Koda is a Dog.", None);
136+
137+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Robbie", "good boy!", 0, String.AlphaNumericUnder);
138+
expect actual == ("Koda is a Dog.", None);
139+
actual := String.SearchAndReplacePosWhole("Koda is a Dog.", "Koda", "Koda", 0, String.AlphaNumericUnder);
140+
expect actual == ("Koda is a Dog.", Some(4));
141+
}
142+
143+
// when forbid comes in to play
144+
method {:test} TestHasSearchAndReplacePosWholeHard()
145+
{
146+
var actual := String.SearchAndReplacePosWhole("KodaisaDog", "Koda", "Robbie", 0, String.AlphaNumericUnder);
147+
expect actual == ("KodaisaDog", None);
148+
actual := String.SearchAndReplacePosWhole("KodaisaDog", "Dog", "Puppy", 1, String.AlphaNumericUnder);
149+
expect actual == ("KodaisaDog", None);
150+
actual := String.SearchAndReplacePosWhole("Koda*isaDog", "Koda", "Robbie", 0, String.AlphaNumericUnder);
151+
expect actual == ("Robbie*isaDog", Some(6));
152+
actual := String.SearchAndReplacePosWhole("Kodaisa.Dog", "Dog", "Puppy", 1, String.AlphaNumericUnder);
153+
expect actual == ("Kodaisa.Puppy", Some(13));
154+
}
155+
156+
// when forbid comes in to play
157+
method {:test} TestHasSearchAndReplaceAllWholeHard()
158+
{
159+
var actual := String.SearchAndReplaceAllWhole("Koda1 Koda Koda2 Koda Koda3", "Koda", "Robbie", String.AlphaNumericUnder);
160+
expect actual == "Koda1 Robbie Koda2 Robbie Koda3";
161+
actual := String.SearchAndReplaceAllWhole("Koda Koda1 Koda Koda2 Koda Koda3 Koda", "Koda", "Robbie", String.AlphaNumericUnder);
162+
expect actual == "Robbie Koda1 Robbie Koda2 Robbie Koda3 Robbie";
163+
}
164+
94165
method {:test} TestHasSubStringPositive()
95166
{
96167
var actual := String.HasSubString("Koda is a Dog.", "Koda");

0 commit comments

Comments
 (0)