-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathfullpaper.tex
4312 lines (3941 loc) · 168 KB
/
fullpaper.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\documentclass[12pt]{article} % may want something different here
\newcommand{\code}[1]{\texttt{#1}} % code examples in text
\newcommand{\reserved}[1]{\textbf{\texttt{#1}}} % reserved words of Larch/C++
\newcommand{\type}[1]{\textrm{\textit{#1}}} % names of types
\newcommand{\RULELAB}[1]{\texttt{#1}}
% a few notations from Dave Schmidt's book
% ``The Structure of Typed Programming Languages'' (MIT Press).
\newcommand{\uminus}{\mbox{$\cup\!\!\!\!-$}}
\newcommand{\udot}{\mbox{$\cup\!\!\!\cdot\,$}}
% formatting boxed displays
\newcommand{\UNSPACEFORBOX}{\vspace{-2ex}}
\newcommand{\HLINE}{\UNSPACEFORBOX%
\begin{flushleft}\rule{\textwidth}{0.01in}\end{flushleft}%
\UNSPACEFORBOX}
\newenvironment{BFIGURE}{
\begin{figure}
\small
\HLINE
}{
\HLINE
\normalsize
\end{figure}
}
\newenvironment{BFIGURE*}{
\begin{figure*}
\HLINE
}{
\HLINE
\end{figure*}
}
%{obey}
% \myobeycr is same as \obeycr, but doesn't do a \@gobblecr.
{\catcode`\^^M=13 \gdef\myobeycr{\catcode`\^^M=13 \def^^M{\\}}%
\gdef\restorecr{\catcode`\^^M=5 }}
% \obeytabs
{\catcode`\^^I=13 \gdef\obeytabs{\catcode`\^^I=13 \def^^I{\hbox{\hskip 4em}}}}
% \obeyspaces
{\obeyspaces\gdef {\hbox{\hskip0.5em}}}
% environment for displayed text, indented, obeys cr, tab, spaces
\newenvironment{obeyDisplay}{%
\samepage%
\begin{list}{}{}\item\obeyspaces\obeytabs\obeycr}{%
\end{list}}
%{grammar}, needs {obey}
%\newcommand{\heading}[1]{\vspace{3ex}{\noindent#1}\vspace{1.5ex}}
\newcommand{\goesto}{\mbox{$::=$}}
\newcommand{\arbno}[1]{#1\mbox{\textrm{*}}}
\newcommand{\nonterm}[1]{\mbox{\it #1}}
\newenvironment{grammar}{
\def\:{\goesto{}}
\def\|{$\vert$}
\tt \myobeycr%
\begin{tabbing}%
\qquad \= $\vert$ \= \qquad \= \kill%
}%
{\unskip\end{tabbing}}
\newenvironment{grammar*}{
\def\:{\goesto{}}
\def\|{$\vert$}
\tt%
\begin{tabbing}%
\qquad \= $\vert$ \= \qquad \= \kill%
}%
{\unskip\end{tabbing}}
\newenvironment{roman-grammar}{
\def\:{\goesto{}}
\def\|{$\vert$}
\myobeycr%
\begin{tabbing}%
\qquad \= $\vert$ \= \qquad \= \kill%
}%
{\unskip\end{tabbing}}
\newenvironment{roman-grammar*}{
\def\:{\goesto{}}
\def\|{$\vert$}
\begin{tabbing}%
\qquad \= $\vert$ \= \qquad \= \kill%
}%
{\unskip\end{tabbing}}
\newenvironment{mathGrammar}{
\def\:{\goesto{}}
\def\|{\hbox{$\vert$}}
\begin{displaymath}%
\tt \obeyspaces%
}%
{\unskip\end{displaymath}}
\addtocounter{tocdepth}{1}
%\documentclass[twoside]{report}
\begin{document}
\begin{titlepage}
\vspace*{1.2in}
\begin{center}
{\LARGE Design and Implementation\\ of the Larch/C++\\ Type System} \\
~ \\
Matthew W. Markland \\
~ \\
\end{center}
\thispagestyle{empty}
\vfill
{\bf Keywords:} Specification languages; Larch; LSL; Larch/C++; Type Systems;.
{\bf 1997 CR Categories:}
\noindent D.1.5 [{\em Programming Techniques}]
Object-oriented Programming
D.2.1 [{\em Software Engineering\/}]
Requirements/Spec\-ifications --- languages, Larch,
tools
D.3.3 [{\em Programming Languages\/}]
Language Constructs and Features --- Modules, packages;
D.3.4 [{\em Programming Languages\/}]
Processors --- Parsing
F.3.1 [{\em Logics and Meanings of Programs\/}]
Specifying and Verifying and Reasoning about Programs ---
assertions, pre- and post-conditions,
specification techniques, LSL
F.3.3 [{\em Logics and Meanings of Programs\/}]
Studies of Program Constructs --- Type Structure
\vspace*{0.2in}
%A version of this paper, without the appendix sections,
%will appear in the proceedings of the
%{\em Colloquium on Formal Approaches in Software Engineering
%(FASE), TAPSOFT '97, Lille, France, April 1996}, to be published by
%Springer-Verlag in their {\em Lecture Notes in Computer Science} Series.
%An earlier version of this paper
%was called ``Protection from the Underspecified''.
%This technical report is also CMU-CS-96-129R.
\copyright{}
Copyright 1997,1998 by Matthew W. Markland.
All rights reserved.
\begin{center}
Department of Computer Science \\
226 Atanasoff Hall \\
Iowa State University \\
Ames, Iowa 50011-1040, USA
\end{center}
\end{titlepage}
\pagenumbering{roman}
\newpage
\tableofcontents
\newpage
\listoffigures
\newpage
\bibliographystyle{plain}
\pagenumbering{arabic}
\setcounter{page}{1}
\author{Matthew W. Markland}
\title{Design and Implementation of the Larch/C++ Type System}
\date{\today}
\maketitle
\begin{abstract}
This paper describes the design of a type system for the Larch/C++
specification language. To motivate the features of the type system,
the type systems of both the Larch Shared Language and C++ are
described. After this background, an informal description of the
Larch/C++ type system is followed by a formalization of that
system. The implementation of an infrastructure for the type system is
then described.
\end{abstract}
%\input{introduction}
\section{Introduction}
\label{introduction}
The goal of Larch/C++ \cite{Leavens96c} is to give the programmer a
formal specification language that is expressive and useful in
practice. The work described in this paper focuses on the addition of
type checking capabilities to the Larch/C++ Checker. In
this context a
\emph{type} is a set of values that exhibit uniform behavior under
a set of associated operations \cite{Watt90}. \emph{Type checking}
defines a process by which a set of formal rules that describe the
type system are applied to operations and statements in a given
specification to decide whether the operations and statements are type
consistent (the terms \emph{sort} and \emph{sort checking} will also
be used interchangeably for type and type checking). The addition of
this functionality allows programmers and specifiers to gain useful
information as to whether the design of a program is sensible and type
consistent before its actual implementation.
Work has been done in the following areas:
\begin{itemize}
\item The creation of a formal description of the Larch/C++ type system.
\item The coding of basic functionality to support the
implementation of the Larch/C++ type system. This work has many
smaller pieces including:
\begin{itemize}
\item Support for User Interaction
\begin{itemize}
\item Improved usability and control over the Larch/C++ Checker via the
creation of a number of command line arguments.
\end{itemize}
\item Support for Larch Shared Language Constructs
\begin{itemize}
\item Modification of the LSL Checker to follow Unix conventions and
use less memory.
\item Development of an interface between the existing Larch/C++ Checker and
the LSL Checker.
\end{itemize}
\item Support for the Evolving C++ Language Standard
\begin{itemize}
\item Support for Draft ANSI Standard C++ \cite{C++Apr95}
language constructs.
\item Support for translation of C++ declarations into Larch/C++
sorts.
\end{itemize}
\end{itemize}
\end{itemize}
The paper begins with a background section that introducing formal
methods, specification, and the Larch/C++ behavioral interface
specification language. Following the general introduction, the type
systems of the Larch Shared Language and C++ are described
briefly. These descriptions motivate a discussion of the basic
functionality of the Larch/C++ type system. This functionality is then
formalized in a description of the sort rules for Larch/C++. Finally
the details of the implementation of the functionality mentioned in
the list above are presented.
\section{Background}
\label{background}
\subsection{Formal Methods}
The information in this section is based upon Wing's
paper \cite{Wing90a}.
Formal methods define processes that are used for software
development. Built upon a mathematical basis, these processes are
designed to reveal ambiguities, incompleteness, and inconsistencies in
software as it is developed \cite{Wing90a}. A formal method will
typically define the specific vocabulary and steps involved in
designing a piece of software.
Formal specifications may be a part of a specific formal
method. \emph{Formal specification} describes a process by which an
abstraction of a problem may be defined and expressed. Usually the
abstraction is expressed in some sort of language specifically
designed for the purpose. Once clearly expressed, the abstraction may serve
as documentation of the problem, a means to communicate the problem
clearly, and/or as a contract defining the problem. Specifications and
their languages are based upon mathematical properties making
them more precise and concise than informal specifications based upon
natural languages. The rigorous definition and mathematical basis
behind formal specification languages also makes it easier to apply machine
analysis and manipulations to them than to specifications in an
informal language \cite{Wing90a}.
Larch/C++ is a behavioral interface specification language. A \emph{behavioral}
specification langauge is used to define an abstraction for a system
based upon thae behavior of that system under certain conditions. In
other words, it describes a system's behavior as observed from the
outside. Larch/C++ describes behavior using a
\emph{model-based} approach; a user builds an abstract model of the system
which describes its behavior. the abstract model becomes a way of
expressing the real world in a manner that can be controlled and
reasoned about. The basic pieces of the model are the interfaces which
exist between the pieces of the system. After a user has described the
behavior in terms of the interfaces, solutions to the problem may then
be designed based up the formal contract defined by the model.
%One common type of formal specification is
%model-based. \emph{Model-based} specification involves the creation
%of an abstract model of the problem that is independent of any actual
%implementation to serve as the specification. The abstract model
%becomes a way of expressing the real world in a manner that can be
%controlled and reasoned about. Once the model has been developed, a
%solution based upon this model can be formalized. Since the solution
%has a rigorous, formal, and mathematical basis, it may be reasoned
%about to decide if it meets the requirements. Once the solution has
%been deemed correct, the specification becomes a formal contract
%describing how the implementation should behave under certain
%conditions.
%There are many different layers at which one may specify a
%problem. Larch/C++ is based upon the idea of behavioral
%specification. \emph{Behavioral specifications} describe the
%constraints on the observable behavior of the items specified. In this
%way, they form a contract between an implementor and a user of the
%implementation.
\subsection{Introduction to Larch/C++}
\label{lcppintro}
Larch/C++ \cite{Leavens96c} is a model-based, formal specification language tailored for
the specification of the behavior of C++ program modules or
application program interfaces (API's). Larch/C++ is not designed to
specify the
behavior of an entire program; instead it allows for the precise,
unambiguous documentation of the behavior C++ program modules
(functions, classes, etc.). Larch/C++ adds syntax to C++ to allow the
specification of complex C++ structures, the inheritance of
specifications, and the clear specification of the interface to a
class.
Larch/C++ is a two-tiered specification language. Specifications
consist of Larch Shared Language (LSL) \cite{Guttag-Horning93} traits
which describe the abstract models, and interface specifications which
formalize the behavioral contracts. This two-tiered approach allows
for the clear separation of the definition of the abstract model and its
vocabulary from the actual details of the programming language modeled
by the interface language. One reason for the separation is so that
the abstract models may be written so that they can be reused in other
specifications. If the abstract models were written in a language
closer to the actual implementation, it would be more difficult to
reuse the same model in a specification for an implementation written
in a different language.
\subsubsection{The Larch Shared Language}
\label{lslintro}
The Larch Shared Language \cite{Guttag-Horning93} allows an user to
supply basic semantic information, and a specialized vocabulary for
describing abstract values. The basic unit of LSL is the
\emph{trait}. Traits contain information on \emph{sorts}, which are
like types in a programming language, and \emph{operators} which define
various operations upon these sorts. Figure~\ref{CounterTrait}
illustrates the LSL portion of a specification for a simple counter
\cite{Leavens96c}. This particular trait illustrates four common
parts that are in many traits. The
\reserved{includes} statement allows for a trait to build upon and
reuse previously written traits. All of the information from the
traits listed in this statement are available in the following
sections of the current trait. Items from the included traits may be
renamed syntactically to make the new trait more readable. This
provides a shortcut for users, allowing them to reuse previous work.
The \reserved{introduces} section defines the abstract model's
operations. In this case, a Counter may be created via
\reserved{newCounter}, or \reserved{inc}, and have its
value reported via \reserved{value}. The
\reserved{asserts} section supplies meaning to these
operations by logically illustrating how the abstract values are
manipulated by the operators. For now, note that a trait defines a
model consisting of a set of abstract values and a set of operations
upon those values. Examples of possible abstract values for the trait
in Figure~\ref{CounterTrait} are \reserved{newCounter}, representing a
brand new counter, and \reserved{inc(newCounter)} representing a
counter that has been incremented once. These values are independent
of any implementation of Counter.
\begin{BFIGURE}
\begin{verbatim}
@(#)$Id: CounterTrait.lsl,v 1.3 1994/12/09 02:48:06 leavens Exp $
CounterTrait: trait
includes Natural(Nat), NoContainedObjects(Counter)
introduces
newCounter: -> Counter
inc: Counter -> Counter
value: Counter -> Nat
Limit: -> Nat
asserts
Counter generated by newCounter, inc
Counter partitioned by value
\forall c: Counter
value(newCounter) == 0;
value(inc(c)) == value(c) + 1;
0 < Limit;
\end{verbatim}
\caption{CounterTrait.lsl}
\label{CounterTrait}
\end{BFIGURE}
\subsubsection{The Larch/C++ Specification Language}
\label{lcppbisl}
Figure~\ref{CounterSpec} contains the Larch/C++ specification
for a class that implements the counter modeled by the previous trait
\cite{Leavens96c}. Larch/C++ specifications consist of a C++ header
file which contains additional annotations set off in speically marked
C++ comments. The use of the comment delimiters, \reserved{//@} and
\reserved{/*@ $\dots$ @*/}, allows the annotations to be easily embedded
directly into new or existing C++ source code. Larch/C++ annotations contain various keywords. In this example, the first section is a
\emph{uses-clause}, which serves a function similar to the \reserved{\#include}
directive in C++; it tells the Larch/C++ Checker the traits that will
be used by this specification. Following that, the next annotations
define a \reserved{spec-variable}, an \reserved{invariant}, and a
\reserved{constraint}. A \reserved{spec-variable} is used to define a
variable which will be used in the specification. The
\reserved{invariant} describes a condition for the C++ class that must
always be true. The \reserved{constraint} describes any limits that
this class must adhere to.
Most individual function specifications
consist of at least three pieces: a requires clause, a modifies
clause, and an ensures clause. The \emph{requires clause} states the
conditions that must be met before an individual function may be
called. If these conditions are not met, there is no guarantee that
the function will run correctly. The \emph{modifies} clause lists all
objects whose state may be initialized or modified by the execution of
this function. Only objects listed
in this clause may change state; thus the modifies clause acts as a
frame axiom. The \emph{ensures clause} serves to state the expected
results of the function provided the conditions specified in the
requires clause were met.
A closer look at the \reserved{increment} function specification illustrates
these sections.
\begin{verbatim}
virtual void increment();
//@ behavior {
//@ requires cnt_value(self^) < Limit;
//@ modifies self;
//@ ensures self' = inc(self^);
//@ }
\end{verbatim}
%\begin{verbatim}
% virtual void increment();
% //@ behavior {
% //@ requires value^ < Limit;
% //@ modifies value;
% //@ ensures value' = value^ + 1;
% //@ }
%\end{verbatim}
\noindent The first line is the C++ prototype for the function. The
\reserved{behavior} keyword announces the beginning of the body of the
specification. The requires clause states that for this function to be
called the value of the counter must be less than the value of
\reserved{Limit}. If it is not, then the behavior of the function is
not specified. If the requires clause is met and function is called,
the modifies clause states that the only possible item that can change
is the counter itself. The ensures clause then states that, if the
previous conditions in the requires clause are met, the value of the counter after the
invocation of this function will be the result of incrementing the
counter.
\begin{BFIGURE}
\begin{verbatim}
// @(#)$Id: Counter.lh,v 1.7 1997/01/12 22:27:38 leavens Exp $
// See J.P. Lejacq's paper in SIGPLAN 26(10), Oct, 1991
//@ uses CounterTrait;
class Counter {
public:
//@ invariant cnt_value(self\any) <= Limit;
//@ constraint cnt_value(self\pre) <= cnt_value(self\post);
Counter();
//@ behavior {
//@ modifies self;
//@ ensures self' = newCounter;
//@ }
virtual int cnt_value() const;
//@ behavior {
//@ ensures result = cnt_value(self^);
//@ }
virtual void increment();
//@ behavior {
//@ requires cnt_value(self^) < Limit;
//@ modifies self;
//@ ensures self' = inc(self^);
//@ }
virtual void reset();
//@ behavior {
//@ modifies self;
//@ ensures cnt_value(self') = 0;
//@ }
};
\end{verbatim}
\caption{Counter.lh}
\label{CounterSpec}
\end{BFIGURE}
%\input{typesystem}
\section{The Type System}
\label{typesystem}
The type system for Larch/C++ is built upon the type systems of LSL
and C++. The process of building a type system involves defining how
the language is scoped, how individual terms are assigned types, and
how the statements and expressions type check. \emph{Scoping} is a
description of the visibility of identifiers. The Larch/C++ type
system bases its assignment of types and rules for type checking
expressions and statements more on the LSL type system, while the
scoping rules are based upon those of C++. This leads to an
interesting algorithm for looking up variables.
Recall that the terms sort and type, and the corresponding
sort checking and type checking, are used interchangeably throuhout
this paper.
\subsection{The LSL Type System}
\label{lslts}
As mentioned earlier in Section~\ref{lslintro} the basic unit of
structure in LSL is the trait. Traits are used to define sorts and
their associated operations, which exhibit uniform behavior under
their associated operations.
Since the Larch/C++ language depends upon LSL to supply
abstractions, it was important to learn how the LSL type system
works. Unfortunately, little has been written on the LSL type
system. Neither the technical report on LSL
\cite{Guttag-Horning-Modet90} nor the Larch book \cite{Guttag-Horning93}
offered any details. What was available was the LSL Checker
\cite{LSLChecker}. The LSL Checker is a tool that will perform semantic and
syntactic checks on LSL traits. Since the LSL Checker provides type
checking of traits, it serves as an operational definition of the
LSL type system. Given this definition, information about the type
system could be generated by running the Checker on example
traits. One option of the LSL Checker that assisted in the development
of the traits, and the initial ideas about the system was its \reserved{-syms}
option. This option will cause the LSL Checker to produce a list of
the operators and their signatures contained within the LSL trait. An
example of this output, generated by the command line \reserved{lsl
-syms Example1.lsl} is illustrated in Figure~\ref{symsoutput} (Note:
this is only a portion of the actual output). Please refer to
Figure~\ref{lslex1} for the trait \reserved{Example1.lsl}, which
generated this output.
\begin{BFIGURE}
\begin{verbatim}
if __ then __ else __: Bool, Bool, Bool -> Bool
if __ then __ else __: Bool, Int, Int -> Int
if __ then __ else __: Bool, int, int -> int
if __ then __ else __: Bool, float, float -> float
true: -> Bool
false: -> Bool
x: -> int
y: -> Bool
f: int -> float
f: int -> Bool
g: Bool -> float
q: int, Bool -> Bool
q: int, Bool -> float
...
\end{verbatim}
\caption{Partial output from the \reserved{lsl -syms} command}
\label{symsoutput}
\end{BFIGURE}
Each line of the \reserved{-syms} output consists of a operator
name and an associated signature for that operator; these parts are separated by a
colon. In the example above, there is an operator named \reserved{x}
which takes no input and returns an item of sort \reserved{int}. There
are also operators such as \reserved{f}, which have two different
signatures. The ability of an operator to have more than one distinct
signature is an example of overloading.\emph{Overloading} occurs when a
given name can simultaneously stand for multiple, distinct
functions.
After examining the \reserved{-syms} output it was clear that LSL
supported overloading. However, the extent of LSL's overloading or its
overload resolution techniques were still unknown. A series of traits
were created that used different sets of functions and the built-in
\texttt{if-then-else} LSL operator. The \texttt{if-then-else} operator
was chosen because it was built-in, because it allowed for
experimentation with types that might not be numeric, and because it
requires the
\reserved{then} and \reserved{else} clauses to have the same unique
sort. The LSL Checker was run on the traits to see what kind of errors,
if any, it found.
\begin{BFIGURE}
\begin{verbatim}
Example1:trait
includes Integer
introduces
x: -> int
y: -> Bool
f: int->float
f: int->Bool
g: Bool->float
q: int,Bool->Bool
q: int,Bool->float
asserts
\forall a:int,b:Bool
q(a,b) == if true then f(a) else g(b);
\end{verbatim}
\caption{Example1.lsl}
\label{lslex1}
\end{BFIGURE}
Figure~\ref{lslex1} is an example of an LSL trait that successfully
sort checks. Working under the assumption that terms could carry sets
of sorts, this trait sort checks in the following way. The term
\reserved{q(a,b)} has the set of sorts
\{\reserved{Bool},\reserved{float}\} associated with it. Similarly the
term \reserved{f(a)} has the set
\{\reserved{float},\reserved{Bool}\}, and the term \reserved{g(b)}
has the set \{\reserved{float}\}. Since the
\reserved{if-then-else} function requires the \reserved{then} and
\reserved{else} clauses to have the same sort, the
resulting sort of this operator must be \reserved{float}. This
illustrates an important point. In this case, the system chooses the
version of operator \reserved{f} that it will use in the type checking
based upon what it needs in the context of the \reserved{if-then-else}
operator. In this case, by choosing the intersection
of the two sets, the LSL Checker chooses to use \reserved{f:~int -> float} because it
works in the context where \reserved{g(b)} only has one sort. This is an
example of context-dependent overload
resolution. \emph{Context-dependent overloading} means that the
context in which the function or variable is used to help uniquely identify
its sort \cite{Watt90}. Finally, since both sides of the \reserved{==}
operator have a sort in common, and it is known from the
\reserved{-syms} output that it requires equivalent sorts for its
arguments, the expression sort checks.
\begin{BFIGURE}
\begin{verbatim}
Example2:trait
includes Integer
introduces
x: -> int
y: -> Bool
f: int->int
f: int->Bool
f: int->E
g: Bool->float
q: int,Bool->Bool
q: int,Bool->float
asserts
\forall a:int,b:Bool
q(a,b) == if true then f(a) else g(b);
\end{verbatim}
\caption{Example2.lsl}
\label{lslex2}
\end{BFIGURE}
Figure~\ref{lslex2} illustrates a situation where the trait will not
sort check. This trait was designed with the purpose of confirming the
assumption made in the above example: that all terms may have sets of
sorts associated with them.
\begin{verbatim}
./Example2.lsl:16: (near col 18): `if __ then __ else __' not
declared with matching domain sorts
Possible sorts for arg 1: Bool
Possible sorts for arg 2: int, Bool, E
Possible sorts for arg 3: float
Abort: error in checking LSL traits
\end{verbatim}
The output from the LSL Checker for this trait describes the possible
sorts available for the arguments to the \reserved{if-then-else}
operation. In this case note that arg 2, which is \reserved{f(a)}, has
three possible sorts. The sort checking error also shows that there
must be an intersection between the sets of the arguments for the
operator to sort check. In this case there is an empty intersection between
\reserved{f(a)}'s set \{\reserved{int},\reserved{Bool},\reserved{E}\}
and \reserved{g(b)}'s set \{\reserved{float}\}. This leads to the
error condition.
\begin{BFIGURE}
\begin{verbatim}
Example3:trait
includes Integer
introduces
x: -> int
y: -> Bool
f: int->int
f: int->Bool
f: int->E
g: Bool->float
g: Bool->int
g: Bool->E
q: int,Bool->Bool
q: int,Bool->float
asserts
\forall a:int,b:Bool
q(a,b) == if true then f(a) else g(b);
\end{verbatim}
\caption{Example3.lsl}
\label{lslex3}
\end{BFIGURE}
To follow up on the previous examples, a trait was created to see if
similar errors could be generated with other operators. This trait is
shown in Figure~\ref{lslex3}.
\begin{verbatim}
./Example3.lsl:18: (near col 8): `q' sorts of terms in equation
do not match
Possible sorts for left side: Bool, float
Possible sorts for right side: int, E
Abort: error in checking LSL traits
\end{verbatim}
\noindent This error shows that the sort associated with the
\reserved{if-then-else} operator is the set consisting of
\{\reserved{int},\reserved{E}\}. So, the LSL Checker will try to find
a sort for \reserved{q(a,b)} that would fit the constraint that
operator \reserved{==} needs to have the same sort for each
argument. In this case, since \reserved{q(a,b)} has the set
\{\reserved{Bool},\reserved{float}\} associated with it, there is no
possible solution.
\begin{BFIGURE}
\begin{verbatim}
Example4:trait
introduces
x: int->int
x: int->float
y: int->int
y: int->float
p: int,int->int
p: int,int->float
asserts
\forall a,b:int
p(a,b) == if (a=b) then x(a) else y(a)
\end{verbatim}
\caption{Example4.lsl}
\label{lslex4}
\end{BFIGURE}
The previous examples have shown that for an operator like
\reserved{==} to sort check, there needs to be a non-empty intersection between
the sets of sorts for its arguments. What if that set has a
cardinality larger than one? Figure~\ref{lslex4} is an example where
the intersection between the sets of sorts for the arguments to
\reserved{==} does not have an intersection of cardinality one. This
generates the following output from the LSL Checker.
\begin{verbatim}
./Example4.lsl:12: (near col 8): `p' more than one possible
sort for terms in equation
Possible sorts: int, float
Abort: error in checking LSL traits
\end{verbatim}
\noindent Since the intersection is not of cardinality one, the
expression does not sort check.
\begin{BFIGURE}
\begin{verbatim}
foo:trait
includes Integer
introduces
x: -> int
y: -> Bool
f: int->float
f: int->Bool
g: Bool->float
q: int,Bool->Bool
q: int,Bool->float
asserts
\forall x:int,b:Bool
q(x,b) == if true then f(x) else g(b);
\end{verbatim}
\caption{A LSL Trait with an Error in the Declaration of Variables}
\label{quanttrait}
\end{BFIGURE}
Another property of the LSL type system is that any variables declared
must have completely unique names. For example the trait in
Figure~\ref{quanttrait} causes the following error to be issued by the
LSL Checker:
\begin{verbatim}
./foo.lsl:15: (near col 9): `x' variable duplicates constant
of same sort
Abort: error in checking LSL traits
\end{verbatim}
\noindent Notice how the \reserved{x:int} declaration within the
\verb+\+\texttt{forall} expression interferes with the \reserved{x: -> int}
declaration in the \reserved{introduces} section. This error occurs
because of constraints placed upon the output the LSL Checker
generates for the Larch Prover.
The results of these experiments with the LSL Checker can be
summarized as follows:
\begin{itemize}
\item LSL terms have non-empty sets of sorts associated with them.
\item The elements in a LSL term's set of sorts may be dependent on
the context in which the term is used.
\item When checking is complete, every expression or equation
should have a single sort. If this does not occur, there is a type error.\item Declared variables should have unique names.
\end{itemize}
\noindent When the system sort checks, there will be sets of sorts
associated with the various terms. As the sort checking progresses,
these sets will be narrowed by the contextual information until every
expression has an assigned, singular sort, or has sort checked.
The other major issue in type systems is scoping. Scoping has few
complications in LSL. There are two scopes, the global scope and
quantifier scope. All names go into the global scope, with the
appropriate overloading, unless they are declared in a quantified
expression.
\begin{BFIGURE}
\begin{verbatim}
asserts
\forall x:E, s1:Set, s2:Set
s1 \subset s2 == \A x (x \in s1 => x \in s2) /\ s1 \neq s2
\end{verbatim}
\caption{An Example of Quantifier Scope.}
\label{quantscope}
\end{BFIGURE}
An example of the creation of quantifier scope is shown in
Figure~\ref{quantscope}. This example shows a portion of a LSL trait
which describes Sets. Notice that the definition of the
\verb+\+\reserved{subset} function contains a quantified
expression of the form \verb+\+\reserved{A x ( $\dots$ )}. The scope
of \reserved{x} is the text between the parentheses.
\subsection{The C++ Type System}
\label{cppts}
This section gives a brief overview of the C++ type
system. Although not a complete description, it should serve as an
introduction for people unfamiliar with it. The section is based upon the C++
Annotated Reference Manual \cite{Ellis-Stroustrup90} which should be
referred to for a complete description of the C++ type system.
The C++ type system is based upon the C type system with a few
additions. There are two broad categories of types, fundamental
types and derived types. \emph{Fundamental types} are the basic
building blocks of the type system. They consist of the types that are
built-in to the implementation. Examples are \reserved{int},
\reserved{float}, and \reserved{char}. \emph{Derived types} are types
built from the fundamental types or from other derived types. Examples of
these include arrays, functions, and classes. Type names can be
created via the \reserved{typedef} construct, which assigns a new name to
a previously existing type.
C++ also offers a variety of polymorphic forms. These include
templates, static overloading, dynamic overloading, and subtype
polymorphism. Although these forms are important to the C++ type
system, with the exception of templates, they are not an important
part of the Larch/C++ type system. Thus it is beyond the scope of this
paper to describe them in more detail.
Templates in C++ let users create generic classes that can be
instantiated to support a specific type. A template allows the
programmer to pass types as parameters to a class. This structure is
an example of parametric polymorphism. \emph{Parametric polymorphism}
is when a set of operations require a type parameter that defines
their behavior.
Compared to LSL, C++ has a complex scope system. The innermost scope
level is local scope. \emph{Local} scope refers to the declarations
within a given block. Items declared with local scope are visible
within the block they are declared in. \emph{Function} scope refers to use of labels within
functions. \emph{Class} scope contains the names of all members, both
functions and variables, that are contained within a class
definition. Finally, \emph{file} scope refers to any declarations that
occur outside of all blocks and classes. Declarations at file scope
are visible within the given translation unit (usually the source
file).
In general, name lookup in C++ begins within the local scope and moves
outward to file scope. The process may be modified by using the scope
resolution (\reserved{::}) operator to state explicitly where to look for the
name. Names may also be hidden or overridden within given scopes. The
key idea is that even with the above features, C++ requires that any
use of a name be unambiguous within a given scope.
\subsection{The Larch/C++ Type System}
\label{lcppts}
\subsubsection{Overview}
The Larch/C++ language has its own unique type system. Though this
system has many things in common with both the LSL and C++ type
systems, Larch/C++ is its own language. Looking at the structure of a
Larch/C++ specification will help to explain the system and its
unique properties. Below is a specification for a simple C++ function
\reserved{increment} which increments a global variable
\reserved{x}. It is based upon the Counter trait shown in Figure~\ref{CounterTrait}.
\begin{verbatim}
int i;
void increment();
//@ behavior {
//@ requires value(i^) < Limit;
//@ modifies i;
//@ ensures i' = inc(i^);
//@ }
\end{verbatim}
\noindent Recall that this specification could be broken down into a
C++ portion and the actual Larch/C++ specification. In this case the line
\begin{verbatim}
int i;
\end{verbatim}
is the C++ declaration for the variable \reserved{i}. The
Larch/C++ type system must be able to take this C++ declaration and
convert it into a binding of i to a sort. This sort can then be used later
when \reserved{i} is mentioned.
The items set off by the \reserved{behavior} keyword are behavioral annotations. It is within this section that the
Larch/C++ system must do its type checking. Within this section, it is
not legal to call an actual C++ function. For example, it would be
illegal to write the following:
\begin{verbatim}
ensures self' = increment();
\end{verbatim}
Thus any terms within the specification that look like functions do not
refer to C++ functions, but rather to LSL operators defined either by
user traits or by the inherent traits for the system. This lack of C++
function calls in the specifications makes the type system simpler. It
does not have to understand the C++ concepts of static and dynamic
overload resolution. It does need to understand LSL operators,
though. Because of this, the Larch/C++ type system acts like the LSL
type system in that it supports operator overloading by creating sets
of sorts for operators, and it will attempt to determine the sorts for
expressions via contextual clues.
The basic notion of the Larch/C++ type system is that there is a
correspondence between C++ declarations and the LSL sorts. Larch/C++
creates this correspondence by having a set of basic sorts which correspond to
the fundamental types in C++. It also adds auxiliary sorts that allow
for the discussion of objects. The Larch/C++ Checker automatically has
these basic sorts available and uses them to convert C++ declarations
into equivalent sorts. Users may also define abstract values and
operations in their own traits. The user would place the trait in a
\reserved{uses} clause before using any theory from it. The
\reserved{uses} clause causes the Larch/C++ Checker to generate
information about the sorts and operations from the trait and make it
available to the rest of the specification.
The \reserved{Uses} clause also supports the C++ template
facility. Since there is no equivalent to parametric polymorphism in
LSL, the \reserved{uses} clause, when combined with renaming, is used
to ``instantiate'' a trait with the correct sort. An example of this
is the SimpleSet specification from the Larch/C++ Manual, Section 8.2
\cite{Leavens96c}. Figure \ref{simpleset} is an example of this
for a simple set class implemented via templates. There is one
template argument, a class \reserved{Elem}, which will be the elements
of the set. The specifier needs to create an abstract model that can
be used with this trait. The specifier creates the following
\reserved{uses} clause for this purpose.
\begin{BFIGURE}
\begin{verbatim}
// @(#)$Id: SimpleSet.lh,v 1.19 1997/06/03 20:29:52 leavens Exp $
template <class Elem>
//@ expects contained_objects(Elem);
//@ where Elem is {
//@ bool operator ==(Elem x, Elem y);
//@ behavior {
//@ ensures returns /\ result = (x = y);
//@ }
//@ };
class Set {
public:
//@ uses SimpleSetTrait(Elem for E, Set<Elem> for C);
Set() throw();
//@ behavior {
//@ constructs self;
//@ ensures liberally self' = empty;