Institute of Computer Science
Faculty of Engineering, Christian-Albrechts-University of Kiel
| Computer-Aided Program
Development Institute of Computer Science Faculty of Engineering, Christian-Albrechts-University of Kiel |
|
| RAP Examples - Evaluation of - Functional Programs |
{***************************************************************************}
{* SYNTAX OF A SUB-LANGUAGE OF FP *}
{***************************************************************************}
type OBJECTS
basedon NAT, BOOL
sort Obj
cons bobj : (Bool)Obj,
nobj : (Nat)Obj,
pair : (Obj,Obj)Obj
endoftype
complete OBJECTS
noetherian OBJECTS
display OBJECTS bobj = "_",
nobj = "_",
pair = "<_,_>"
type FORMS
basedon ID, NAT, BOOL
sort Form
cons id, p_1, p_2, {Id., Proj.}
eqz, s, p, ad, su, mu : Form, {Basisfct. NAT}
bconst : (Bool)Form,
nconst : (Nat)Form,
iconst : (Id)Form,
comp, tuple : (Form,Form)Form,
cond : (Form,Form,Form)Form
endoftype
complete FORMS
noetherian FORMS
display FORMS bconst = "_~",
nconst = "_~",
iconst = "_",
comp = "(_ o _)",
tuple = "[_, _]",
cond = "if _\ then _\ else _\endif"
type DECLARATIONS
basedon FORMS, ID, BOOL
sort Decls
cons emptydecls : Decls,
declare : (Decls,Id,Form)Decls
func body : (Decls,Id)Form
axioms all (i,j : Id, e : Decls, f : Form)
body(declare(e,i,f),i) -> f,
equal_Id(i,j) = false => body(declare(e,i,f),j) -> body(e,j)
endoftype
complete DECLARATIONS except body
noetherian DECLARATIONS
display DECLARATIONS emptydecls = "",
declare = "_\_ <= _"
{***************************************************************************}
{* EVALUATION *}
{***************************************************************************}
type FP
basedon DECLARATIONS, FORMS, OBJECTS, ID, NAT, BOOL
func eval : (Decls,Form,Obj)Obj
axioms all (a, b : Bool, m, n : Nat, f, g, h : Form, x, y : Obj,
e : Decls, i : Id)
eval(e,id,x) -> x,
eval(e,p_1,pair(x,y)) -> x,
eval(e,p_2,pair(x,y)) -> y,
eval(e,iconst(i),x) -> eval(e,body(e,i),x),
eval(e,eqz,nobj(n)) -> bobj(equal_Nat(n,0)),
eval(e,s,nobj(n)) -> nobj(succ(n)),
eval(e,p,nobj(n)) -> nobj(pred(n)),
eval(e,ad,pair(nobj(m),nobj(n))) -> nobj(add(m,n)),
eval(e,su,pair(nobj(m),nobj(n))) -> nobj(sub(m,n)),
eval(e,mu,pair(nobj(m),nobj(n))) -> nobj(mult(m,n)),
eval(e,bconst(a),x) -> bobj(a),
eval(e,nconst(m),x) -> nobj(m),
eval(e,comp(f,g),x) -> eval(e,g,eval(e,f,x)),
eval(e,tuple(f,g),x) -> pair(eval(e,f,x),eval(e,g,x)),
eval(e,f,x) = bobj(false) =>
eval(e,cond(f,g,h),x) -> eval(e,h,x),
eval(e,f,x) = bobj(true) =>
eval(e,cond(f,g,h),x) -> eval(e,g,x)
endoftype
complete FP
noetherian FP
display FP eval = "_;\_ <_>\"
{***************************************************************************}
{* SOME EXAMPLES FOR EVALUATIONS OF FP-PROGRAMS *}
{***************************************************************************}
task FAC6
basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
unknown x: Obj
goals x = eval(declare(
emptydecls,
'Fac, cond(eqz,
nconst(1),
comp(tuple(id,comp(p,iconst('Fac))),mu))),
comp(s,iconst('Fac)),
nobj(5)
)
endoftask
task EVE3
basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT, BOOL
unknown x: Obj
goals x = eval(declare(declare(
emptydecls,
'Odd, cond(eqz,
bconst(false),
comp(p,iconst('Eve)))),
'Eve, cond(eqz,
bconst(true),
comp(p,iconst('Odd)))),
iconst('Eve),
nobj(3)
)
endoftask
task DUP7
basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
unknown x: Obj
goals x = eval(declare(
emptydecls,
'Dup, cond(eqz,
nconst(0),
comp(comp(comp(p,iconst('Dup)), s), s))),
iconst('Dup),
nobj(7)
)
endoftask
task FAC3T2
basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
unknown x: Obj
goals x = eval(declare(declare(declare(
emptydecls,
'Fac, cond(eqz,
nconst(1),
comp(tuple(id,comp(p,iconst('Fac))),mu))),
'Dup, cond(eqz,
nconst(0),
comp(comp(p,iconst('Dup)),iconst('Ad2)))),
'Ad2, comp(s,s)),
comp(iconst('Fac),iconst('Dup)),
nobj(3)
)
endoftask
task FAC3T2X
basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT
unknown dec : Decls, exp : Form, inp, res : Obj
goals dec = declare(declare(declare(
emptydecls,
'Fac, cond(eqz,
nconst(1),
comp(tuple(id,comp(p,iconst('Fac))),mu))),
'Dup, cond(eqz,
nconst(0),
comp(comp(p,iconst('Dup)),iconst('Ad2)))),
'Ad2, comp(s,s)),
exp = comp(iconst('Fac),iconst('Dup)),
inp = nobj(3),
res = eval(dec,exp,inp)
endoftask
{***************************************************************************}
{* SOME GLOBAL DECLARATIONS FOR THE SUBSEQUENT PROOFS *}
{***************************************************************************}
type GLOBALS
basedon DECLARATIONS, OBJECTS
func d : Decls, y : Obj
endoftype
{***************************************************************************}
{* PROOF OF f o [g,h] = [f o g, f o h] *}
{***************************************************************************}
task PROOF1
basedon FP, FORMS, OBJECTS, GLOBALS
unknown f, g, h : Form
goals eval(d,comp(f,tuple(g,h)),y)
= eval(d,tuple(comp(f,g),comp(f,h)),y)
endoftask
{***************************************************************************}
{* PROOF OF f o (g o h) = (f o g) o h) *}
{***************************************************************************}
task PROOF2
basedon FP, FORMS, OBJECTS, GLOBALS
unknown f, g, h : Form
goals eval(d,comp(f,comp(g,h)),y)
= eval(d,comp(comp(f,g),h),y)
endoftask
{***************************************************************************}
{* PROOF OF A DISTRIBUTIVITY PROPERTY *}
{***************************************************************************}
task PROOF3
basedon FP, FORMS, OBJECTS, GLOBALS
unknown f, g, h, k : Form
goals eval(d, comp(cond(f,g,h),k),y)
= eval(d,cond(f,comp(g,k),comp(h,k)),y)
endoftask
{***************************************************************************}
{* A PROOF USING TERM INDUCTION *}
{***************************************************************************}
task PROOF4
basedon FP, DECLARATIONS, FORMS, OBJECTS, ID, NAT, BOOL
unknown d: Decls, n : Nat
goals d = declare(declare(emptydecls,
'Odd, cond(eqz,
bconst(false),
comp(p,iconst('Eve)))),
'Eve, cond(eqz,
bconst(true),
comp(p,iconst('Odd)))),
eval(d,iconst('Eve),nobj(n)) = eval(d,iconst('Odd),nobj(succ(n)))
endoftask