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.