From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 357BEBBAF; Tue, 24 Mar 2009 11:07:30 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnwHAN9NyEmAXTcZ/2dsb2JhbACNLQHEe4N2Bg X-IronPort-AV: E=Sophos;i="4.38,412,1233529200"; d="scan'208";a="23145956" Received: from deby.inria.fr ([128.93.55.25]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 24 Mar 2009 11:07:29 +0100 Received: from deby.inria.fr (weis@localhost.inria.fr [127.0.0.1]) by deby.inria.fr (8.14.3/8.14.3) with ESMTP id n2OA7T6t019110; Tue, 24 Mar 2009 11:07:29 +0100 (CET) Received: (from weis@localhost) by deby.inria.fr (8.14.3/8.14.3/Submit) id n2OA7TQj025998; Tue, 24 Mar 2009 11:07:29 +0100 (CET) Date: Tue, 24 Mar 2009 11:07:29 +0100 (CET) From: Pierre Weis Message-Id: <200903241007.n2OA7TQj025998@deby.inria.fr> To: caml-announce@inria.fr, caml-list@inria.fr, coq-announce@inria.fr, coq-list@inria.fr, focalize-users@inria.fr Subject: First release of focalize, a development environment for high integrity programs. X-Spam: no; 0.00; weis:01 weis:01 bug:01 compiler:01 coq:01 compiler:01 redefinition:01 coq:01 vastly:01 syntax:01 semantics:01 hunters:98 featuring:98 2009:98 incremental:01 Hi to all of you careful bug hunters and happy hackers reading this message! It is my pleasure to announce the first public release for FoCaLize, a purely functional language and environment to express and formally prove algorithms and their implementation. (0) What is it ? ---------------- FoCaLize is an integrated development environment to write high integrity programs and systems. It provides a purely functional language to formally express specifications, describe the design and code the algorithms. Within the functional language, FoCaLize provides a logical framework to express the properties of the code. A simple declarative language provides the natural expression of proofs of those properties from within the program source code. The FoCaLize compiler extracts statements and proof scripts from the source file, to pass them to the Zenon proof generator that produces in turn the Coq proof terms that are formally verified. The FoCaLize compiler also generates the code corresponding to the program as an Objective Caml source file. This way, programs developped in FoCaLize can be efficiently compiled to native code on a large variety of architectures. Last but not least, FoCaLize automatically generates the documentation corresponding to the development, a requirement for high evaluation assurance. The FoCaLize system provides means for the developers to formally express their specifications and to go step by step (in an incremental approach) to design and implementation, while proving that such an implementation meets its specification or design requirements. The FoCaLize language offers high level mechanisms such as inheritance, late binding, redefinition, parametrization, etc. Confidence in proofs submitted by developers or automatically done relies on Coq formal proof verification. FoCaLize is a son of the previous Focal system. However, it is a completely new implementation with vastly revised syntax and semantics, featuring a rock-solid infrastructure and greatly improved capabilities. (1) Where to find it ? ---------------------- FoCaLize home page is http://FoCaLize.inria.fr/ FoCaLize source files can be found at http://FoCaLize.inria.fr/download/focalize-0.1.0.tgz (2) How to install it ? ----------------------- Uncompress, extract, then read the INSTALL file in the newly created directory focalize.0.1.0 and follow the simple instructions written there. Enjoy. For the entire FoCaLize implementor group, Pierre Weis. Tuesday, March 24, 2009 10:05:13