It's a long way off yet! But I have just committed the first
cut of some code which generated input to the Why program:
http://why.lri.fr/
You'll get a file looking like that shown below at the moment:
/////////////////
(****** HACKS *******)
type 'a lvalue (* Felix lvalues *)
type dunno (* translation error *)
type ('a,'b) fn (* functions *)
(****** ABSTRACT TYPES *******)
(* type ostream, at ./lib/std.flx: line 518, cols 3 to 33 *)
type ostream
(* type string, at ./lib/flx_ctypes.flxh: line 224, cols 1 to 28 *)
type string
(* type char, at ./lib/flx_ctypes.flxh: line 20, cols 5 to 23 *)
type char
(* type int, at ./lib/flx_ctypes.flxh: line 25, cols 5 to 21 *)
(* type int -- USE why's builtin *)
(* type iterator, at ./lib/std.flx: line 1797, cols 7 to 36 *)
type iterator
(* type double, at ./lib/flx_ctypes.flxh: line 34, cols 5 to 27 *)
type double
(****** UNIONS *******)
(* type opt, at ./lib/std.flx: line 59 col 3 to line 62 col 3 *)
type 'T opt
(****** STRUCTS *******)
(******* FUNCTIONS ******)
(* function mod, at ./lib/flx_ctypes.flxh: line 176, cols 3 to 32 *)
logic mod_1950: 'T1947, 'T1947 -> 'T1947
(* function diveq, at ./lib/flx_ctypes.flxh: line 177, cols 3 to 40 *)
logic diveq_1951: 'T1947 lvalue , 'T1947 -> unit
(* function modeq, at ./lib/flx_ctypes.flxh: line 178, cols 3 to 40 *)
logic modeq_1952: 'T1947 lvalue , 'T1947 -> unit
.......
(******* AXIOMS ******)
(* axiom distrib, at ./lib/flx_tclass.flxh: line 70, cols 3 to 61 *)
(* axiom assoc, at ./lib/flx_tclass.flxh: line 62, cols 3 to 48 *)
(* axiom sym, at ./lib/flx_tclass.flxh: line 41, cols 3 to 34 *)
(* axiom assoc, at ./lib/flx_tclass.flxh: line 37, cols 3 to 48 *)
/////////////////
So what's this all about?
Felix supports various kinds of assertions: assert, preconditions
and postconditions for functions, reductions, and axioms in
typeclasses. We'd also like to support theorems.
The Why program is a translator that takes a fixed language,
the Why language, and translated it into proof obligations
in the form required by various common theorem provers and
proof assistants.
So the basic idea is to translate Felix assertions into Why
assertions, use Why to translate them into input for a prover,
run the prover, and report the result. With any luck we might
be able to actually prove some simple properties of things.
Initially, it probably makes sense to restrict the scope
of what we will try to prove. I'm thinking of adding
'theorems' to typeclasses, and trying to prove them.
Note that Why does not handle translation of proofs into
a form which can be verified by proof assistants ..
however some of the programs try to prove things without
help, so we can try them.
I have no idea if this will work or be useful, but there's
only one way to find out!
--
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net
-------------------------------------------------------------------------
Using Tomcat but need to do more? Need to support web services, security?
Get stuff done quickly with pre-integrated technology to make your job easier.
Download IBM WebSphere Application Server v.1.0.1 based on Apache Geronimo
http://sel.as-us.falkag.net/sel?cmd=lnk&kid=120709&bid=263057&dat=121642
_______________________________________________
Felix-language mailing list
Felix-language@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/felix-language
