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

Copyright | (c) Joel Burget Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | Safe-Inferred
Language | Haskell2010

Data.SBV.String

Contents

- Length, emptiness
- Deconstructing/Reconstructing
- Containment
- Substrings
- Reverse
- Conversion to/from naturals

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 :: SString -> SInteger
- null :: SString -> SBool
- head :: SString -> SChar
- tail :: SString -> SString
- uncons :: SString -> (SChar, SString)
- init :: SString -> SString
- singleton :: SChar -> SString
- strToStrAt :: SString -> SInteger -> SString
- strToCharAt :: SString -> SInteger -> SChar
- (!!) :: SString -> SInteger -> SChar
- implode :: [SChar] -> SString
- concat :: SString -> SString -> SString
- (.:) :: SChar -> SString -> SString
- snoc :: SString -> SChar -> SString
- nil :: SString
- (++) :: SString -> SString -> SString
- isInfixOf :: SString -> SString -> SBool
- isSuffixOf :: SString -> SString -> SBool
- isPrefixOf :: SString -> SString -> SBool
- take :: SInteger -> SString -> SString
- drop :: SInteger -> SString -> SString
- subStr :: SString -> SInteger -> SInteger -> SString
- replace :: SString -> SString -> SString -> SString
- indexOf :: SString -> SString -> SInteger
- offsetIndexOf :: SString -> SString -> SInteger -> SInteger
- reverse :: SString -> SString
- strToNat :: SString -> SInteger
- natToStr :: SInteger -> SString

# Length, emptiness

length :: SString -> SInteger Source #

Length of a string.

    >>> sat $ \s -> length s .== 2
    Satisfiable. Model:
      s0 = "BA" :: 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 -> 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 :: 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 = "AB" :: 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 -> i `inRange` (0, length s - 1) .&& s `strToCharAt` i .== c .=> indexOf s (singleton c) .<= i Q.E.D.

(!!) :: SString -> SInteger -> SChar Source #

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.

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

Concatenate two strings. See also `++`.

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

Prepend an element, the traditional `cons`.

snoc :: SString -> SChar -> SString Source #

Append an element

nil :: SString Source #

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 :: 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 .s .= indexOf s (subStr s i 1) .<= i Q.E.D.

    >>> 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.

# Reverse

reverse :: SString -> SString Source #

``reverse` s` reverses the string. >>> sat $ s -> reverse s .== "abc" Satisfiable. Model: s0 = "cba" :: String >>> prove $ s -> reverse s .== "" .= null s 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'.

    >>> prove $ \s -> let n = strToNat s in length s .== 1 .=> (-1) .<= n .&& n .<= 9
    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.

    >>> prove $ \i -> length (natToStr i) .== 3 .=> i .<= 999
    Q.E.D.