Quelle WWellForm.thy

Sprache: Isabelle

(*  Title:      JinjaDCI/J/WWellForm.thy

    Author:     Tobias Nipkow, Susannah Mansky
    Copyright   2003 Technische Universitaet Muenchen, 2019-20 UIUC

    Based on the Jinja theory J/WWellForm.thy by Tobias Nipkow
*)

section ‹ Weak well-formedness of Jinja programs ›

theory WWellForm imports "../Common/WellForm" Expr begin

definition wwf_J_mdecl :: "J_prog ==> cname ==> J_mb mdecl ==> bool"
where
  "wwf_J_mdecl P C ≡ λ(M,b,Ts,T,(pns,body)).
length Ts = length pns ∧ distinct pns ∧ ¬sub_RI body ∧
  (case b of
   NonStatic ==> this ∉ set pns ∧ fv body ⊆ {this} ∪ set pns
| Static ==> fv body ⊆ set pns)"

lemma wwf_J_mdecl_NonStatic[simp]:
  "wwf_J_mdecl P C (M,NonStatic,Ts,T,pns,body) =
  (length Ts = length pns ∧ distinct pns ∧ ¬sub_RI body ∧ this ∉ set pns ∧ fv body ⊆ {this} ∪ set pns)"
(*<*)by(simp add:wwf_J_mdecl_def)(*>*)

lemma wwf_J_mdecl_Static[simp]:
  "wwf_J_mdecl P C (M,Static,Ts,T,pns,body) =
  (length Ts = length pns ∧ distinct pns ∧ ¬sub_RI body ∧ fv body ⊆ set pns)"
(*<*)by(simp add:wwf_J_mdecl_def)(*>*)

abbreviation
  wwf_J_prog :: "J_prog ==> bool" where
  "wwf_J_prog ≡ wf_prog wwf_J_mdecl"

lemma sees_wwf_nsub_RI:
"[ wwf_J_prog P; P ⊨ C sees M,b : Ts→T = (pns, body) in D ] ==> ¬sub_RI body"
(*<*)by(auto dest!: sees_wf_mdecl simp: wwf_J_mdecl_def wf_mdecl_def)(*>*)

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.