products/sources/formale Sprachen/Isabelle/HOL/IMP image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: README.txt   Sprache: Text

Original von: Isabelle©

theory C_like imports Main begin

subsection "A C-like Language"

type_synonym state = "nat \ nat"

datatype aexp = N nat | Deref aexp ("!") | Plus aexp aexp

fun aval :: "aexp \ state \ nat" where
"aval (N n) s = n" |
"aval (!a) s = s(aval a s)" |
"aval (Plus a\<^sub>1 a\<^sub>2) s = aval a\<^sub>1 s + aval a\<^sub>2 s"

datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp

primrec bval :: "bexp \ state \ bool" where
"bval (Bc v) _ = v" |
"bval (Not b) s = (\ bval b s)" |
"bval (And b\<^sub>1 b\<^sub>2) s = (if bval b\<^sub>1 s then bval b\<^sub>2 s else False)" |
"bval (Less a\<^sub>1 a\<^sub>2) s = (aval a\<^sub>1 s < aval a\<^sub>2 s)"


datatype
  com = SKIP 
      | Assign aexp aexp         ("_ ::= _" [61, 61] 61)
      | New    aexp aexp
      | Seq    com  com          ("_;/ _"  [60, 61] 60)
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

inductive
  big_step :: "com \ state \ nat \ state \ nat \ bool" (infix "\" 55)
where
Skip:    "(SKIP,sn) \ sn" |
Assign:  "(lhs ::= a,s,n) \ (s(aval lhs s := aval a s),n)" |
New:     "(New lhs a,s,n) \ (s(aval lhs s := n), n+aval a s)" |
Seq:    "\ (c\<^sub>1,sn\<^sub>1) \ sn\<^sub>2; (c\<^sub>2,sn\<^sub>2) \ sn\<^sub>3 \ \
          (c\<^sub>1;c\<^sub>2, sn\<^sub>1) \<Rightarrow> sn\<^sub>3" |

IfTrue:  "\ bval b s; (c\<^sub>1,s,n) \ tn \ \
         (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s,n) \<Rightarrow> tn" |
IfFalse: "\ \bval b s; (c\<^sub>2,s,n) \ tn \ \
         (IF b THEN c\<^sub>1 ELSE c\<^sub>2, s,n) \<Rightarrow> tn" |

WhileFalse: "\bval b s \ (WHILE b DO c,s,n) \ (s,n)" |
WhileTrue:
  "\ bval b s\<^sub>1; (c,s\<^sub>1,n) \ sn\<^sub>2; (WHILE b DO c, sn\<^sub>2) \ sn\<^sub>3 \ \
   (WHILE b DO c, s\<^sub>1,n) \<Rightarrow> sn\<^sub>3"

code_pred big_step .

declare [[values_timeout = 3600]]

text\<open>Examples:\<close>

definition
"array_sum =
 WHILE Less (!(N 0)) (Plus (!(N 1)) (N 1))
 DO ( N 2 ::= Plus (!(N 2)) (!(!(N 0)));
      N 0 ::= Plus (!(N 0)) (N 1) )"

text \<open>To show the first n variables in a \<^typ>\<open>nat \<Rightarrow> nat\<close> state:\<close>
definition 
  "list t n = map t [0 ..< n]"

values "{list t n |t n. (array_sum, nth[3,4,0,3,7],5) \ (t,n)}"

definition
"linked_list_sum =
 WHILE Less (N 0) (!(N 0))
 DO ( N 1 ::= Plus(!(N 1)) (!(!(N 0)));
      N 0 ::= !(Plus(!(N 0))(N 1)) )"

values "{list t n |t n. (linked_list_sum, nth[4,0,3,0,7,2],6) \ (t,n)}"

definition
"array_init =
 New (N 0) (!(N 1)); N 2 ::= !(N 0);
 WHILE Less (!(N 2)) (Plus (!(N 0)) (!(N 1)))
 DO ( !(N 2) ::= !(N 2);
      N 2 ::= Plus (!(N 2)) (N 1) )"

values "{list t n |t n. (array_init, nth[5,2,7],3) \ (t,n)}"

definition
"linked_list_init =
 WHILE Less (!(N 1)) (!(N 0))
 DO ( New (N 3) (N 2);
      N 1 ::=  Plus (!(N 1)) (N 1);
      !(N 3) ::= !(N 1);
      Plus (!(N 3)) (N 1) ::= !(N 2);
      N 2 ::= !(N 3) )"

values "{list t n |t n. (linked_list_init, nth[2,0,0,0],4) \ (t,n)}"

end

¤ Dauer der Verarbeitung: 0.24 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




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 ist noch experimentell.


Bot Zugriff