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

Copyright(c) Joel Burget Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Data.SBV.String

Contents

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 :: SString -> SInteger Source #

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 :: SString -> SBool Source #

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 :: SString -> SChar Source #

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

>>> prove $ \c -> head (singleton c) .== c
Q.E.D.

tail :: SString -> SString Source #

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 -> bnot (null s) ==> singleton (head s) .++ tail s .== s
Q.E.D.

init :: SString -> SString Source #

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 :: SChar -> SString Source #

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 :: SString -> SInteger -> SString Source #

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\EOT" :: String

strToCharAt :: SString -> SInteger -> SChar Source #

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.

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.

concat :: SString -> SString -> SString Source #

Concatenate two strings. See also .++.

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

Prepend an element, the traditional cons.

(.++) :: 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 :: SString -> SString -> SBool Source #

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 :: SString -> SString -> SBool Source #

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 :: SString -> SString -> SBool Source #

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 :: SInteger -> SString -> SString Source #

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 :: SInteger -> SString -> SString Source #

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 :: SString -> SInteger -> SInteger -> SString Source #

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 :: SString -> SString -> SString -> SString Source #

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 :: SString -> SString -> SInteger Source #

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 = "\NUL\NUL\NUL\NUL\NUL" :: String
  s1 =                      3 :: Integer
>>> prove $ \s1 s2 -> length s2 .> length s1 ==> indexOf s1 s2 .== -1
Q.E.D.

offsetIndexOf :: SString -> SString -> SInteger -> SInteger Source #

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 :: SString -> SInteger Source #

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 :: SInteger -> SString Source #

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.