perm filename EIGHT[BIB,CSR] blob
sn#495779 filedate 1980-02-08 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00019 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 .turn on "↔" for "→"
C00005 00003 PVG-16↔(STAN-CS-80-789)
C00007 00004 2
C00008 00005 3
C00009 00006 4
C00010 00007 5
C00011 00008 6
C00012 00009 7
C00013 00010 8
C00014 00011 9
C00015 00012 10
C00016 00013 11
C00017 00014 12
C00018 00015 13
C00019 00016 14
C00020 00017 15
C00021 00018 16
C00022 00019 17
C00023 ENDMK
C⊗;
.turn on "↔" for "→"
.turn on "%,π,α,#,&,∂,↑,↓,[,]"
.turn on "∩" for "↑"
.turn on "∪" for "↓"
.at "@" ⊂"####"⊃
.next page
.begin center
S T A N F O R D U N I V E R S I T Y
MOST RECENT COMPUTER SCIENCE REPORTS - 1980
.end
No. 8↔April
@Listed here are abstracts of the most recent reports published by the
Department of Computer Science at Stanford University.
@TO REQUEST REPORTS: Check the appropriate places on the enclosed order
form, and return the entire order form page (including mailing label) by
June 30, 1980. In many cases we can print only a limited number of copies,
and requests will be filled on a first come, first served basis. If the code
(FREE) is printed on your mailing label, you will not be charged for hardcopy.
This exemption from payment is limited primarily to libraries. (The costs
shown include all applicable sales taxes. PLEASE SEND NO MONEY NOW, WAIT UNTIL
YOU GET AN INVOICE.)
@ALTERNATIVELY: Copies of most Stanford CS Reports may be obtained by writing
(about 2 months after the "MOST RECENT CS REPORTS" listing) to NATIONAL
TECHNICAL INFORMATION SERVICE, 5285 Port Royal Road, Springfield, Virginia 22161.
Stanford Ph.D. theses are available from UNIVERSITY MICROFILMS, 300 North
Zeeb Road, Ann Arbor, Michigan 48106.
.BEGIN NOFILL
---------------------------------------------------------------------
---------------------------------------------------------------------
PVG-16↔(STAN-CS-80-789)
"ADA EXCEPTIONS : SPECIFICATION AND PROOF TECHNIQUES"
Authors: D. C. Luckham and W. Polak
pages↔Cost: $
.end
@A method of documenting exception propagation and handling in Ada programs
is proposed. Exception propagation declarations are introduced as a new
component of Ada specifications. This permits documentation of those
exceptions that can be propagated by a subprogram. Exception handlers are
documented by entry assertions. Axioms and proof rules for Ada exceptions
are given. These rules are simple extensions of previous rules for Pascal
and define an axiomatic semantics of Ada exceptions. As a result, Ada
programs specified according to the method can be analysed by formal proof
techniques for consistency with their specifications, even if they employ
exception propagation and handling to achieve required results (i.e. non
error situations). Example verifications are given.
.begin nofill
---------------------------------------------------------------------
2
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
3
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
4
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
5
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
6
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
7
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
8
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
9
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
10
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
11
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
12
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
13
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
14
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
15
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
16
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
17
"
Author:
pages↔Cost: $
.end
@
.begin nofill
---------------------------------------------------------------------
---------------------------------------------------------------------