On 23/12/2010, at 3:46 AM, Claude Marche wrote:
>
>
> We are happy to announce the first public release of Why3, also known
> as the Why platform next generation. It is a new project, independent
> from Why versions 2.xx.
> 3) Source code organized as a library with a documented API,
> to allow access to Why3 features programmatically.
Nice!
Couple of questions: any students around to help with integration tasks? :)
Note to Erick: Why3 is using git, investigate making a submodule.
Description: Felix has a Why2 module as part of the translator (currently
disabled
due to lack of resources to maintain it).
The programming language Felix has a minimal and probably badly designed
assertional facility intended to allow programmers to actually specify some
semantics: in this it is fairly unique. Here's an example, as part of a type
class:
// equality
typeclass Eq[t] {
virtual fun eq: t * t -> bool;
virtual fun ne (x:t,y:t):bool => not (eq (x,y));
axiom reflex(x:t): eq(x,x);
axiom sym(x:t, y:t): eq(x,y) == eq(y,x);
axiom trans(x:t, y:t, z:t): implies(eq(x,y) and eq(y,z), eq(x,z));
}
It's possible to also assert lemmas, which are Why proof obligations.
The interface to Ergot via Why2 has actually succeeded in proving one lemma!
--
john skaller
[email protected]
------------------------------------------------------------------------------
Learn how Oracle Real Application Clusters (RAC) One Node allows customers
to consolidate database storage, standardize their database environment, and,
should the need arise, upgrade to a full multi-node Oracle RAC database
without downtime or disruption
http://p.sf.net/sfu/oracle-sfdevnl
_______________________________________________
Felix-language mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/felix-language
