[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Question about With

Hi,

As my understanding 'WITH' can be use to define constraint
over a partial function.
I try to built 'env' and 'builtEnv' function which generate the
constraint over 'env'.
I define a lemma that I hope can do the evaluation recursively.
Where is my mistakes ?

Below is my codes.

Thank's for your help.

******

 env: TYPE = [extNode -> signal[boolean]]
 staticData: TYPE = [# name:extNode, val:signal[bool] #]

 builtEnv (el1:env, el2:list[staticData]) : RECURSIVE env =
    CASES el2 OF
      null: el1,
      cons(hd,tl): let a=name(hd)
                             in builtEnv(el1 with [a:=val(hd)],tl)
    ENDCASES
  MEASURE length(el2)

 env_lm1 : LEMMA
    FORALL (env1:env,name1,name2:extNode,val1:signal[bool]) :
      (env1 with [name1:=val1])(name2) =
        IF name1=name2 THEN val1 ELSE env1(name2) ENDIF

****** 

-- 
Kong Woei susanto
Department of Computing Science - University of Glasgow
17 Lilybank Gardens, Glasgow G12 8RZ, Scotland, United Kingdom.
e-mail: susanto@dcs.gla.ac.uk Ph: +44-141-3304454  fax:+44-141-3304913