DEFINITION MODULE DString;
(* gm2-style opaque dynamic string: TYPE String; completed in the
   implementation (DynamicStrings model). *)
TYPE String;
PROCEDURE Make(n : INTEGER) : String;
PROCEDURE Get(s : String) : INTEGER;
PROCEDURE IsNil(s : String) : BOOLEAN;
END DString.