Quelle Var.thy

Sprache: Isabelle

section ‹UTP variables›

theory Var
imports Main
begin

text ‹UTP variables are characterized by two functions, $select$ and $update$.
The variable type is then defined as a tuple ($select$ * $update$).›

type_synonym ('a, 'r) var = "('r ==> 'a) * (('a ==> 'a) ==> 'r ==> 'r)"

text ‹The $lookup$ function returns the corrsponding $select$ function of a variable.›

definition lookup :: "('a, 'r) var ==> 'r ==> 'a"
  where "lookup f ≡ (fst f)"

text ‹The $assign$ function uses the $update$ function of a variable to update its value.›

definition assign :: "('a, 'r) var ==> 'a ==> 'r ==> 'r"
  where "assign f v ≡ (snd f) (λ _ . v)"

text ‹The $VAR$ function allows to retrieve a variable given its name.›

syntax "_VAR" :: "id ==> ('a, 'r) var"  (‹VAR _›)
translations "VAR x" => "(x, _update_name x)"

end

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.2 Sekunden ¤

Wurzel

Suchen

NIST Cobol Testsuite

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.