Literals

Literals: Concepts, Issues, and Designs

Literals

Literals are simple notation for denoting specific objects. In Specware, Nat, Char, and String literals are built-in. Other literals can be defined using these. For example, (nat-to-integer 14). Note that while these literals are built-in, they are virtual in the current system (Specware 2.0): they exist only in the surface syntax. Their internal representation is as a construction using the appropriate constructors. In particular: Nat literals are represented as binary terms; Char literals are represented as (nat-to-char <nat-literal>); and, String literals are constructed using Char literals, empty-string, and prepend-string. Here is an example of the basic literals. 
spec lit-test-00 is
 axiom (equal n 123)
 axiom (equal c 'D')
 axiom (equal s "aBc")
 end-spec
Nat Literals
Char Literals
String Literals
Nat literals
Nat literals are built-in in Specware. The syntax is the usual: (equal n 123)
An example of use is in: nat-literal-use.re
Char literals
In Specware, Char literals are built-in. The syntax is C-like: (equal c 'K') Here is a sample of the different Char literals; note that @ and \ require special treatment. Also, see the Specweb page for CHAR. 
spec char-literal-use is

  axiom (equal chr 'c')
  axiom (equal chr 'C')
  axiom (equal chr '\@')
  axiom (equal chr '\\')
  axiom (equal chr ''')  
  axiom (equal chr '`')
  axiom (equal chr ' ')
  axiom (equal chr '.')
  axiom (equal chr '
')
  axiom (equal chr '0')
  axiom (equal chr '!')
  axiom (equal chr '#')
  axiom (equal chr '$')
  axiom (equal chr '%')
  axiom (equal chr '&')
  axiom (equal chr '(')
  axiom (equal chr ')')
  axiom (equal chr '*')
  axiom (equal chr '+')
  axiom (equal chr ',')
  axiom (equal chr '-')
  axiom (equal chr '/')
  axiom (equal chr ':')
  axiom (equal chr ';')
  axiom (equal chr '<')
  axiom (equal chr '=')
  axiom (equal chr '>')
  axiom (equal chr '?')
  axiom (equal chr '[')
  axiom (equal chr ']')
  axiom (equal chr '^')
  axiom (equal chr '_')
  axiom (equal chr '{')
  axiom (equal chr '|')
  axiom (equal chr '}')
  axiom (equal chr '~')
  axiom (equal chr '"')
 end-spec
String Literals
String literals are constructed using Char literals, empty-string, and prepend-string. The surface syntax of String literals is the usual: "<seq-of-Char>" For example, "a1B2c3", "456", and "" are String literals. The Chars allowed in Strings are those in char.re. See the Specweb page for CHAR. Here is are some examples of string literals. 
spec string-literal-use is
  axiom (equal str "aBc")
  axiom (equal str "123")
  axiom (equal str "4C@\\'` .
0!#$%&()*+,-/:;<=>?[]^_{|}~\"")
end-spec


SpecWeb Index Specs