Go to the first, previous, next, last section, table of contents.


11.9 Character Strings

Character strings are not really a type in C++, but merely a convention for using character arrays in which a null (0) character is found. To help state the pre- and postconditions of functions that deal with C++ strings, Larch/C++ provides the following LSL trait. Unlike the other traits in this chapter, the traits in this section are not implicitly used by Larch/C++. You have to write a uses clause to use one or more of them. (see section 9.2 The Uses Clause for how to use a trait).

The following trait can be used with the C++ types char * and the corresponding array types. Recall that the abstract values of pointers of type char * have sort Ptr[Obj[char]] (see section 11.8 Pointer Types). Recall that the abstract values of arrays of characters have sort Arr[Obj[char]] (see section 11.7 Array Types). However, recall that, when used in a formal parameter declaration, both char * and char [] stand for the sort Ptr[Obj[char]] (see section 6.1.8.1 Sorts for Formal Parameters).

% @(#)$Id: cpp_char_string.lsl,v 1.25 1995/11/06 16:02:59 leavens Exp $
% Compare Guttag and Horning's book (Springer-Verlag, 1994), page 64

cpp_char_string: trait

  includes int, char, TypedObj(Obj, char),
           Pointer(Obj, char),
           String(char, String[char], int for Int)

  introduces
    null: -> char
    nullTerminated: Ptr[Obj[char]], State -> Bool
    nullTerminated: Arr[Obj[char]], State -> Bool
    throughNull: Ptr[Obj[char]], State -> String[char]
    throughNull: Arr[Obj[char]], State -> String[char]
    uptoNull: Ptr[Obj[char]], State -> String[char]
    uptoNull: Arr[Obj[char]], State -> String[char]
    sameCharsThroughNull: Ptr[Obj[char]], State, Ptr[Obj[char]], State -> Bool
    sameCharsThroughNull: Arr[Obj[char]], State, Ptr[Obj[char]], State -> Bool
    sameCharsThroughNull: Ptr[Obj[char]], State, Arr[Obj[char]], State -> Bool
    sameCharsThroughNull: Arr[Obj[char]], State, Arr[Obj[char]], State -> Bool
    lengthToNull: Ptr[Obj[char]], State -> int
    lengthToNull: Arr[Obj[char]], State -> int
    objectsToNull: Ptr[Obj[char]], State -> Set[Object]
    objectsToNull: Arr[Obj[char]], State -> Set[Object]
    legalStringIndex: Ptr[Obj[char]], State, int -> Bool
    legalStringIndex: Arr[Obj[char]], State, int -> Bool

  asserts
    \forall p, p1, p2: Ptr[Obj[char]], st, st1, st2: State, i: int,
            a, a1, a2: Arr[Obj[char]]
      null == 0;

      nullTerminated(p, st) ==
        assigned(p,st) /\ (eval(*p,st) = null \/ nullTerminated(p+1,st));
      nullTerminated(a, st) == nullTerminated(address_of(a,0), st);

      nullTerminated(p, st)
        => (throughNull(p, st)
             = (if eval(*p,st) = null then {null}
                else eval(*p,st) \precat throughNull(p+1,st)));
      throughNull(a, st) == throughNull(address_of(a,0), st);

      nullTerminated(p, st)
        => (uptoNull(p, st)
             = (if eval(*p,st) = null then empty
                else eval(*p,st) \precat uptoNull(p+1,st)));
      uptoNull(a, st) == uptoNull(address_of(a,0), st);

      (nullTerminated(p1, st1) /\ nullTerminated(p2, st2))
        => (sameCharsThroughNull(p1, st1, p2, st2) =
             (throughNull(p1,st1) = throughNull(p2,st2)));
      sameCharsThroughNull(a1, st1, p2, st2) ==
        sameCharsThroughNull(address_of(a1,0), st1, p2, st2);
      sameCharsThroughNull(p1, st1, a2, st2) ==
        sameCharsThroughNull(p1, st1, address_of(a2,0), st2);
      sameCharsThroughNull(a1, st1, a2, st2) ==
        sameCharsThroughNull(address_of(a1,0), st1, address_of(a2,0), st2);

      nullTerminated(p, st)
        => (lengthToNull(p, st) = len(throughNull(p,st)) - 1);
      lengthToNull(a, st) == lengthToNull(address_of(a,0), st);

      nullTerminated(p, st)
        => (objectsToNull(p,st) = (if eval(*p,st) = null then {widen(*p)}
                                 else {widen(*p)} \U objectsToNull(p+1,st)));
      objectsToNull(a, st) == objectsToNull(address_of(a,0), st);

      nullTerminated(p, st)
        => (legalStringIndex(p, st, i) = (0 <= i /\ i < lengthToNull(p,st)));
      legalStringIndex(a, st, i) == legalStringIndex(address_of(a,0), st, i);

  implies converts null, nullTerminated: Ptr[Obj[char]], State -> Bool,
                   nullTerminated: Arr[Obj[char]], State -> Bool

The above trait also gives a good example of when one needs to use states explicitly in a trait. The trait function nullTerminated, for example, can only tell if a null character is in a string by examining the abstract values of the character objects in a given state. See section 2.8.2 Formal Model of States for more about states. See section 2.8.1 Formal Model of Objects for more about the trait TypedObj that defines eval.

A trait that renames some of the sorts used in the cpp_string trait is given below. This trait is useful when dealing with the C++ types const char * and the corresponding array types. Recall that the abstract values of such pointers have sort Ptr[ConstObj[char]], and the abstract values of the corresponding arrays have sort Arr[ConstObj[char]].

% @(#)$Id: cpp_const_char_string.lsl,v 1.5 1995/01/04 03:16:31 leavens Exp $
cpp_const_char_string: trait
   includes cpp_char_string(ConstObj for Obj)

As an example of how to use these traits, the following is the specification of a strcpy function, which copies the characters in s2 into s1. (The following specification may or may not specify strcpy from any particular standard or library.)

// @(#)$Id: strcpy.lh,v 1.12 1997/06/03 20:30:21 leavens Exp $
extern char* strcpy(char *s1, const char *s2) throw();
//@ behavior {
//@   uses cpp_char_string, cpp_const_char_string;
//@   requires nullTerminated(s2, pre)
//@            /\ allocatedUpTo(s1, lengthToNull(s2, pre) + 1, pre);
//@   modifies objectsInRange(s1, 0, lengthToNull(s2, pre));
//@   ensures result = s1 /\ nullTerminated(s1,post)
//@           /\ sameCharsThroughNull(s1, post, s2, pre);
//@ }

The Larch/C++ release also contains a trait cpp_unsignedChar_string for dealing with the C++ types unsigned char * and unsigned char [] as strings. There is also a trait cpp_wchar_t_string for dealing with the C++ types wchar_t * and wchar_t [] as strings. Both of these traits are similar to cpp_const_string. The following trait can be used to include all the relevant traits.

% @(#)$Id: cpp_string.lsl,v 1.3 1995/07/26 21:18:43 leavens Exp $
% trait for C++ strings of various types
cpp_string: trait
  includes cpp_char_string, cpp_const_char_string,
           cpp_unsignedChar_string, cpp_const_unsignedChar_string,
           cpp_wchar_t_string, cpp_const_wchar_t_string


Go to the first, previous, next, last section, table of contents.