《java语言的异常处理机制的公理语义》由会员分享，可在线阅读，更多相关《java语言的异常处理机制的公理语义（71页珍藏版）》请在金锄头文库上搜索。
1、大连理工大学 硕士学位论文 Java语言的异常处理机制的公理语义 姓名：曲文敬 申请学位级别：硕士 专业：计算机应用技术 指导教师：王树义 20040301 摘要 本文以J a v a 语言为背景，讨论异常处理机制的公理语义。主要工作包含四部分： ( 1 ) 详细地讨论了t h r o w 语句和t r y 语句的公理语义。 ( 2 ) 给出了与异常处理机制密切相关的运算符n e w 和c o n t i n u e ，b r e a k ，r e t u r n 等语 句的公理语义。 ( 3 ) 为了说明本文提出的公理语义方案具有一般性，也给出了具有异常处理机制条件 下，i f 语句，w h
2、 il e 语句，和块等语句的公理语义。 ( 4 ) 最后给出一个具有异常处理功能的程序片段的正确性证明的实例。 关于公理语义，目前没有见到讨论c o n t i n u e ，b r e a k ，r e t u r n 等的语句的公理化方 面的文章，主要原因是这些语句涉及到控制转移问题，用逻辑公式不易描述。 对于异常处理机制来说，其公理语义的研究难度更大。因为，异常处理机制涉及到 更大范围的控制转移，这种转移可能是跨函数或者跨文件的。根据J a v a 异常处理机制 的语义，一旦发生异常，在查找处理该异常的过程中，可能会终止一连串的方法调用。 为了描述控制转移，引入一个变量R E A S
3、O N ，它记录每个语句执行结束后，该语句的执 行状态。根据这个状态，决定控制的走向。因此，在每个语句，表达式的公理中的条件 部分和结论部分都含有R g A S O N 。条件部分的R E A S O N 决定程序下步执行所选择的公理； 而结论部分的R E A S O N ，用来决定程序下一步执行的条件，从而解决了用公理语义的方 法描述的更大范围的控制转移问题。 关键字：J a v a 异常处理机制。J a v a 语言，公理化，程序验证 A b s t r a c t I nt h i St h e s i Sa x i o m a t i cs e m a n t i c so fJ a
4、v ae x c e p t i o nh a n d l i n gm e c h a n i s mi S i n t r o d u c e d T h ec o n t e n do fp a p e ri sd i v i d e di n t of o u rp a r t s ： ( i ，O i S O U S St h ea x i o m a t i cs e m a n t i c so ft h r o wa n dt r ys t a t e m e n t ( 2 ) G i v et h ea x i o m a t i cs e m a n t i c so f
5、t h eo p e r a t o r 一- n e wa n dc o n t i n u e b r e a ka n d r e t u r ns t a t e m e n t ，w h i c ha r ec o n c e r n i n ga b o u tt h ee x c e p t i o n h a n d l i n g ( 3 ) W ea l S Og i v et h ea x i o m a t i cs e m a n t i c so fi fs t a t e m e n ta n dw h i l es t a t e m e n ta n d b
6、l o c ks t a t e m e n ti no r d e rt os h o wt h a tt h ea x i o m a t i cs e m a n t i c sp l a ni Sn o r m a l ( 4 ) A tl a s t ，w eg i v ea ne x a m p l eo ft h ec o r r e c t n e s so fc o d es l i c e 。w h i c hh a st h e e x c e p t i o nh a n d li n g A b o u tt h ea x i o m a t i Cs e m a n
7、 t i C S Ih a v en o ts e et h ea r t i c l e sa b o u tt h e a x i o m a t i cs e m a n t i O So fc o n t i n u e ，b r e a k ，r e t u r n ，a n dt h em a i nr e a s o ni St h e s e s t a t e m e n t sc o n c e r n i n ga b o u tt h ec o n t r o lt r a n s f e ra n dd i f f i c u l t l vt od e s c r
8、i b e t h ef o r m u l a I ot h ee x c e p t i o nh a n d l i n gm e c h a n i s m ，t h ea x i o m a t i cs e m a n t i c si Sd i f f i c u l t l Y t or e s e a r c h T h ee x c e p t i o nh a n d l i n gm e c h a n i s mc o n c e r n i n gl a r g e s c a l ec o n t r o l t r a n s f e r S Ot h et r
9、 a n s f e ri Sp r o b a b l Yb e t w e e nt h ef u n c t i o n so rf i l e s W h e nt h e e x c e p t i o n sh a p p e n ，i nt h ep r o c e s so fh a n d l i n gt h ee x c e p t i o n ，as e r i e so ff u n c t i o n c a l l i n gw i l lt e r m i n a t e T ot h ec o n t r o lt r a n s f e r ，av a r
10、i a b l eR E A S O Ni Si n t r o d u c e d ， w h i c hi sr e c o r d e de v e r ys t a t eo fs t a t e m e n te x e c u t i o n T h es t a t e sd e c i d et h e c o n t r 0 1t r a n s f e r S o i ne v e r ys t a t e m e n t ，t h ec o n d i t i o no rc o n c l u s i o no ft h e d x i o m a t i Cs e m
11、 a n t i C So fe x p r e s s i o nh a st h e “R E A S O N ”T h ec o n d ic i o no ft h e R E A S O Nd e c i d et h ea x i o md e c i d et h en e x ts t e po ft h ep r o g r a mr u n n i n g O e s c r i b i o g t h es t a t eo fe v e r yp o i n to fc o d ea n da d d i n gs o m er u l e r ，w ec a ng e
12、 tt h ec o r r e c t n e s s o fC h ep r o g r a m U s i n gt h ea x i o m a t i Cs e m a n t i C Sw es o l v et h ep r o b l e mt h a td e s c r i b e t h el a r g e s c a l ec o n t r o lt r a n s f e r K e y w o r d ：e x c e p t i O Nh a n d Ii n gm e c h a n i s mo fJ a v a ，J a v ap r o g r a m
13、 m i n gI a n g u a g e a x i o m a t i cs e m a n t i C S p r o g r a mv e r i f i c a t i o n J a v a 语言的异常处理机制的公理语义 O 前言 0 1 采用异常处理机制的必要性 在程序开发中，程序员在编写程序时发生错误时在所难免的。对于包含错误的程序， 我们该如何做使其纠正这些错误，使其正确? 这些错误是如何被处理的? 谁处理的? 程 序可以被正确的恢复吗? 或就是简单的让它中止? 要解决这些问题，以往在面向过程程序设计语言中，利用返回值，做一个简单的判 断，再给出相应的处理，这个方法在简单
14、情况下，小系统中能给出一个较好的解决。但 在大型软件开发中，往往用这种方法实现起来很难，甚至是根本难以实现，并会人为的 使程序代码复杂化。丽大型软件开发本身就是一个难题，面向对象技术在一定程度上降 低了其开发难度，更重要的是它实现了异常处理机制。 由程序语言提供的异常处理机制简化了开发强壮的软件系统的难度。使用这些机制， 软件开发者可以描述在一个模块中异常的发生条件，在模块执行中出现异常，在出现的 那一时刻就会被处理。异常的处理机制，在其中起着举足轻重的作用。异常处理机制已 经不仅仅被当作汇报错误的一种机制，在程序员开发实践中，也被用来作为处理程序非 正状态一种处理机制。 从局部的观点看，要生
15、成一个强壮的系统，开发者必须分析清楚模块中异常的流程。 在面向对象语言中，使用未经检查的异常，使得软件开发者难于对其进行针对性的处理。 特别的，J a v a 语言结构的异常流程( f l o wo fe x c e p t i o n ) 使得用户可以加入自己设想的 对异常的处理。 为了简化了开发强壮的软件系统的难度，很多现代的程序语言都有一个异常处理机制。 这些机制主要是；在一个程序点，通过某种手段明确产生异常的情况和另外一些手段提 供一组代码去处理异常情况。在本质上，这些机制提供给软件开发者一种方法，把处理 异常情况的代码与那些处理一般情况的代码分离，这有助于软件开发者从逻辑上和结构 上
16、组织代码。 很多情况下，仅从局部是无法分析清楚一个错误的产生原因的。一些简单的应用中，可 以在异常发生的时刻，产生异常信息并终止程序的运行。在另一些应用中，则更希望或 者能恢复异常，或为终止程序提供一些有用的信息。所以，异常处理机寿l 应运面生，并 较好的解决了这些问题。 J a v a 语言使用异常来提供针对其程序的错误处理能力。异常就是一个再程序正常运行状 态下发生的事件。如果，你编写过J a v a 程序，那你一定会遇到异常。你第一次遇到的J a v a 程序的异常从编译器带来的错误信息也许是这样的： I n p u t F i l e j a v a ：1 l ：E x c e p t i o nj a v a i o F i l e N o t F o u n d E x c e p t i o nm u s tb ec a u g h t ，o r i tm u s tb ed e c l a r e di nt h et h r o w sc l a u s e o ft h i sm e
