sbv-8.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Data.SBV.String

Description

A collection of string/character utilities, useful when working with symbolic strings. To the extent possible, the functions in this module follow those of Data.List so importing qualified is the recommended workflow. Also, it is recommended you use the OverloadedStrings extension to allow literal strings to be used as symbolic-strings.

Synopsis

# Length, emptiness

Length of a string.

>>> sat $\s -> length s .== 2 Satisfiable. Model: s0 = "\NUL\NUL" :: String >>> sat$ \s -> length s .< 0
Unsatisfiable
>>> prove $\s1 s2 -> length s1 + length s2 .== length (s1 .++ s2) Q.E.D.  null s is True iff the string is empty >>> prove$ \s -> null s .<=> length s .== 0
Q.E.D.
>>> prove $\s -> null s .<=> s .== "" Q.E.D.  # Deconstructing/Reconstructing head returns the head of a string. Unspecified if the string is empty. >>> prove$ \c -> head (singleton c) .== c
Q.E.D.


tail returns the tail of a string. Unspecified if the string is empty.

>>> prove $\h s -> tail (singleton h .++ s) .== s Q.E.D. >>> prove$ \s -> length s .> 0 .=> length (tail s) .== length s - 1
Q.E.D.
>>> prove $\s -> sNot (null s) .=> singleton (head s) .++ tail s .== s Q.E.D.  uncons :: SString -> (SChar, SString) Source # @uncons returns the pair of the first character and tail. Unspecified if the string is empty. init returns all but the last element of the list. Unspecified if the string is empty. >>> prove$ \c t -> init (t .++ singleton c) .== t
Q.E.D.


singleton c is the string of length 1 that contains the only character whose value is the 8-bit value c.

>>> prove $\c -> c .== literal 'A' .=> singleton c .== "A" Q.E.D. >>> prove$ \c -> length (singleton c) .== 1
Q.E.D.


strToStrAt s offset. Substring of length 1 at offset in s. Unspecified if offset is out of bounds.

>>> prove $\s1 s2 -> strToStrAt (s1 .++ s2) (length s1) .== strToStrAt s2 0 Q.E.D. >>> sat$ \s -> length s .>= 2 .&& strToStrAt s 0 ./= strToStrAt s (length s - 1)
Satisfiable. Model:
s0 = "\NUL\NUL\DLE" :: String


strToCharAt s i is the 8-bit value stored at location i. Unspecified if index is out of bounds.

>>> prove $\i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" strToCharAt i .== literal 'A' Q.E.D. >>> prove$ \s i c -> s strToCharAt i .== c .=> indexOf s (singleton c) .<= i
Q.E.D.


Short cut for strToCharAt

implode :: [SChar] -> SString Source #

implode cs is the string of length |cs| containing precisely those characters. Note that there is no corresponding function explode, since we wouldn't know the length of a symbolic string.

>>> prove $\c1 c2 c3 -> length (implode [c1, c2, c3]) .== 3 Q.E.D. >>> prove$ \c1 c2 c3 -> map (strToCharAt (implode [c1, c2, c3])) (map literal [0 .. 2]) .== [c1, c2, c3]
Q.E.D.


Concatenate two strings. See also .++.

(.:) :: SChar -> SString -> SString infixr 5 Source #

Prepend an element, the traditional cons.

Append an element

Empty string. This value has the property that it's the only string with length 0:

>>> prove $\l -> length l .== 0 .<=> l .== nil Q.E.D.  (.++) :: SString -> SString -> SString infixr 5 Source # Short cut for concat. >>> sat$ \x y z -> length x .== 5 .&& length y .== 1 .&& x .++ y .++ z .== "Hello world!"
Satisfiable. Model:
s0 =  "Hello" :: String
s1 =      " " :: String
s2 = "world!" :: String


# Containment

isInfixOf sub s. Does s contain the substring sub?

>>> prove $\s1 s2 s3 -> s2 isInfixOf (s1 .++ s2 .++ s3) Q.E.D. >>> prove$ \s1 s2 -> s1 isInfixOf s2 .&& s2 isInfixOf s1 .<=> s1 .== s2
Q.E.D.


isSuffixOf suf s. Is suf a suffix of s?

>>> prove $\s1 s2 -> s2 isSuffixOf (s1 .++ s2) Q.E.D. >>> prove$ \s1 s2 -> s1 isSuffixOf s2 .=> subStr s2 (length s2 - length s1) (length s1) .== s1
Q.E.D.


isPrefixOf pre s. Is pre a prefix of s?

>>> prove $\s1 s2 -> s1 isPrefixOf (s1 .++ s2) Q.E.D. >>> prove$ \s1 s2 -> s1 isPrefixOf s2 .=> subStr s2 0 (length s1) .== s1
Q.E.D.


# Substrings

take len s. Corresponds to Haskell's take on symbolic-strings.

>>> prove $\s i -> i .>= 0 .=> length (take i s) .<= i Q.E.D.  drop len s. Corresponds to Haskell's drop on symbolic-strings. >>> prove$ \s i -> length (drop i s) .<= length s
Q.E.D.
>>> prove $\s i -> take i s .++ drop i s .== s Q.E.D.  subStr s offset len is the substring of s at offset offset with length len. This function is under-specified when the offset is outside the range of positions in s or len is negative or offset+len exceeds the length of s. >>> prove$ \s i -> i .>= 0 .&& i .< length s .=> subStr s 0 i .++ subStr s i (length s - i) .== s
Q.E.D.
>>> sat  $\i j -> subStr "hello" i j .== "ell" Satisfiable. Model: s0 = 1 :: Integer s1 = 3 :: Integer >>> sat$ \i j -> subStr "hell" i j .== "no"
Unsatisfiable


replace s src dst. Replace the first occurrence of src by dst in s

>>> prove $\s -> replace "hello" s "world" .== "world" .=> s .== "hello" Q.E.D. >>> prove$ \s1 s2 s3 -> length s2 .> length s1 .=> replace s1 s2 s3 .== s1
Q.E.D.


indexOf s sub. Retrieves first position of sub in s, -1 if there are no occurrences. Equivalent to offsetIndexOf s sub 0.

>>> prove $\s i -> i .> 0 .&& i .< length s .=> indexOf s (subStr s i 1) .<= i Q.E.D. >>> prove$ \s i -> i .> 0 .&& i .< length s .=> indexOf s (subStr s i 1) .== i
Falsifiable. Counter-example:
s0 = "\128\NUL\NUL" :: String
s1 =              2 :: Integer
>>> prove $\s1 s2 -> length s2 .> length s1 .=> indexOf s1 s2 .== -1 Q.E.D.  offsetIndexOf s sub offset. Retrieves first position of sub at or after offset in s, -1 if there are no occurrences. >>> prove$ \s sub -> offsetIndexOf s sub 0 .== indexOf s sub
Q.E.D.
>>> prove $\s sub i -> i .>= length s .&& length sub .> 0 .=> offsetIndexOf s sub i .== -1 Q.E.D. >>> prove$ \s sub i -> i .> length s .=> offsetIndexOf s sub i .== -1
Q.E.D.


# Conversion to/from naturals

strToNat s. Retrieve integer encoded by string s (ground rewriting only). Note that by definition this function only works when s only contains digits, that is, if it encodes a natural number. Otherwise, it returns '-1'. See http://cvc4.cs.stanford.edu/wiki/Strings for details.

>>> prove $\s -> let n = strToNat s in n .>= 0 .&& n .< 10 .=> length s .== 1 Q.E.D.  natToStr i. Retrieve string encoded by integer i (ground rewriting only). Again, only naturals are supported, any input that is not a natural number produces empty string, even though we take an integer as an argument. See http://cvc4.cs.stanford.edu/wiki/Strings for details. >>> prove$ \i -> length (natToStr i) .== 3 .=> i .<= 999
Q.E.D.