本文以Java语言为背景，讨论异常处理机制的公理语义。主要工作包含四部分： (1) 详细地讨论了throw语句和try语句的公理语义。 (2) 给出了与异常处理机制密切相关的运算符new和continue，break，return等语句的公理语义。 (3) 为了说明本文提出的公理语义方案具有一般性，也给出了具有异常处理机制条件下，if语句，while语句，和块等语句的公理语义。 (4) 最后给出一个具有异常处理功能的程序片段的正确性证明的实例。 关于公理语义，目前没有见到讨论continue，break，return等的语句的公理化方面的文章，主要原因是这些语句涉及到控制转移问题，用逻辑公式不易描述。 对于异常处理机制来说，其公理语义的研究难度更大。因为，异常处理机制涉及到更大范围的控制转移，这种转移可能是跨函数或者跨文件的。根据Java异常处理机制的语义，一旦发生异常，在查找处理该异常的过程中，可能会终止一连串的方法调用。为了描述控制转移，引入一个变量REASON，它记录每个语句执行结束后，该语句的执行状态。根据这个状态，决定控制的走向。因此，在每个语句，表达式的公理中的条件部分和结论部分都含有REASON。条件部分的REASON决定程序下一步执行所选择的公理；而结论部分的REASON，用来决定程序下一步执行的条件，从而解决了用公理语义的方法描述的更大范围的控制转移问题。