| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/JinjaDCI/Common/ (Archive of formal Proofs Version 2026-5©) Datei vom 29.4.2026 mit Größe 1 kB |
|
Quelle Value.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* Title: Jinja/Common/Value.thy Author: David von Oheimb, Tobias Nipkow Copyright 1999 Technische Universitaet Muenchen *) section ‹ Jinja Values › theory Value imports TypeRel begin type_synonym addr = nat datatype val = Unit ― ‹dummy result value of void expressions› | Null ― ‹null reference› | Bool bool ― ‹Boolean value› | Intg int ― ‹integer value› | Addr addr ― ‹addresses of objects in the heap› primrec the_Intg :: "val → int" where "the_Intg (Intg i) = i" primrec the_Addr :: "val → addr" where "the_Addr (Addr a) = a" primrec default_val :: "ty → val" ― ‹default value for all types› where "default_val Void = Unit" | "default_val Boolean = Bool False" | "default_val Integer = Intg 0" | "default_val NT = Null" | "default_val (Class C) = Null" end
¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01