Library Prelude
This file is part of
A Formal Definition of JML in Coq
and its Application to Runtime Assertion Checking
Ph.D. Thesis by Hermann Lehner
Online available at jmlcoq.info
Authors:
- Hermann Lehner
- David Pichardie (Bicolano)
- Andreas Kaegi (Syntax Rewritings, Implementation of ADTs)
Require Import JMLProgramPlusImpl.
Require Import ZArith.
Module java.
Module lang.
Definition PKG_lang_ : PackageName := Program.PKG_lang_.
Definition C_Object_ : ShortClassName := 1%Z.
Definition Object_ : ClassName := (PKG_lang_, C_Object_).
Definition C_Integer_ : ShortClassName := 2%Z.
Definition Integer_ : ClassName := (PKG_lang_, C_Integer_).
Definition C_String_ : ShortClassName := 3%Z.
Definition String_ : ClassName := (PKG_lang_, C_String_).
Definition C_Exception_ : ShortClassName := Program.C_Exception_.
Definition Exception_ : ClassName := (PKG_lang_, C_Exception_).
Definition C_CloneNotSupportedException_ : ShortClassName := 5%Z.
Definition CloneNotSupportedException_ : ClassName := (PKG_lang_, C_CloneNotSupportedException_).
Definition C_RuntimeException_ : ShortClassName := 6%Z.
Definition RuntimeException_ : ClassName := (PKG_lang_, C_RuntimeException_).
Definition C_IllegalArgumentException_ : ShortClassName := 7%Z.
Definition IllegalArgumentException_ : ClassName := (PKG_lang_, C_IllegalArgumentException_).
Definition C_Throwable_ : ShortClassName := 8%Z.
Definition Throwable_ : ClassName := (PKG_lang_, C_Throwable_).
Definition C_Error_ : ShortClassName := 9%Z.
Definition Error_ : ClassName := (PKG_lang_, C_Error_).
Module Object.
Parameter M_Object_1 : MethodSignature.
Parameter M_toString_2 : MethodSignature.
Parameter M_finalize_3 : MethodSignature.
Parameter M_clone_4 : MethodSignature.
Parameter M_hashCode_5 : MethodSignature.
End Object.
Module Integer.
Parameter M_Integer_1 : MethodSignature.
Parameter M_intValue_2 : MethodSignature.
Parameter M_toString_3 : MethodSignature.
Parameter M_toString_4 : MethodSignature.
Parameter M_min_5 : MethodSignature.
Parameter F_MAX_VALUE : FieldSignature.
End Integer.
Module String.
Parameter M_length_1 : MethodSignature.
End String.
Module Long.
Parameter M_min_5 : MethodSignature.
Parameter F_MAX_VALUE : FieldSignature.
End Long.
End lang.
End java.
Module org.
Module jmlspecs.
Module models.
Definition PKG_models_ : PackageName := 2%Z.
Definition C_JMLObjectSet_ : ShortClassName := 10%Z.
Definition JMLObjectSet_ : ClassName := (PKG_models_, C_JMLObjectSet_).
Module JMLObjectSet.
Parameter M_has_1 : MethodSignature.
End JMLObjectSet.
End models.
End jmlspecs.
End org.