11 This theory provides definitions for the @{text Object} class, |
11 This theory provides definitions for the @{text Object} class, |
12 and the system exceptions. |
12 and the system exceptions. |
13 *} |
13 *} |
14 |
14 |
15 definition ObjectC :: "'c cdecl" where |
15 definition ObjectC :: "'c cdecl" where |
16 "ObjectC \<equiv> (Object, (undefined,[],[]))" |
16 [code_inline]: "ObjectC \<equiv> (Object, (undefined,[],[]))" |
17 |
17 |
18 definition NullPointerC :: "'c cdecl" where |
18 definition NullPointerC :: "'c cdecl" where |
19 "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))" |
19 [code_inline]: "NullPointerC \<equiv> (Xcpt NullPointer, (Object,[],[]))" |
20 |
20 |
21 definition ClassCastC :: "'c cdecl" where |
21 definition ClassCastC :: "'c cdecl" where |
22 "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))" |
22 [code_inline]: "ClassCastC \<equiv> (Xcpt ClassCast, (Object,[],[]))" |
23 |
23 |
24 definition OutOfMemoryC :: "'c cdecl" where |
24 definition OutOfMemoryC :: "'c cdecl" where |
25 "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))" |
25 [code_inline]: "OutOfMemoryC \<equiv> (Xcpt OutOfMemory, (Object,[],[]))" |
26 |
26 |
27 definition SystemClasses :: "'c cdecl list" where |
27 definition SystemClasses :: "'c cdecl list" where |
28 "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" |
28 [code_inline]: "SystemClasses \<equiv> [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC]" |
29 |
29 |
30 end |
30 end |