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
---------------------------------------------------------------------
---------------------------------------------------------------------