K-user mailing list

[Gurvan Le Guernic <gleguern AT gmail.com>]

   Hi,

 I have previously used K to define a language semantics. In the context of an industrial R&D project, I would want to try a more complex project with can, but am not sure it is doable currently with K.

 I have a language L to define data packets (sequence of fields of different types). I want to :
1. define an encoding semantics Se for L (the semantics Se of a program in L and a sequence of values is a bit string) [this should be OK] ;
2. define a decoding semantics Sd for L (the semantics Sd of a program in L and a bit string is a sequence of values) [this should be OK] ;
3. prove a few properties on Se and Sd, for example (Sd o Se)(l) is the identity function for a meaningfull domain [is it doable in K ?] ;
4. define a compilation algorithm Alg_e for L that takes a program P in L and produces a Verilog (or C) program that has the same semantics as Se for P (and do the same for Sd and an algorithm Alg_d) [I should be able to do that thru rewriting rules that transform a L program into a Verilog program ] ;
5. prove the equivalence (bisimulation) between Se[P] and Verilog[Alg_e(P)] (and do the same for Sd and Alg_d).

 I would rather not start this project as is if I can not achieve it with K.
 Does the current implementation of K provides (mature enough) tools to do this project ?
 Which tools would you suggest I use to prove/verify the properties of Se and Sd (point 3) and prove/verify the bisimulation relation (point 5) ?
 Have others done a similar thing, or do you have advices for this project ?
 Can I reuse the specifications of C and Verilog in the projects webpage ? Do they still work with the current version of K ?

   Thank you very much for any help you could provide,
   Gurvan