From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.3 required=5.0 tests=BAYES_00,XPRIO, XPRIO_SHORT_SUBJ autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,dce17094f2aeee50,start X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-08-06 09:58:24 PST Path: archiver1.google.com!newsfeed.google.com!newsfeed.stanford.edu!canoe.uoregon.edu!logbridge.uoregon.edu!newsfeed1.cidera.com!cyclone2.usenetserver.com!usenetserver.com!news01.optonline.net!news02.optonline.net.POSTED!not-for-mail From: "programmer" Newsgroups: comp.lang.ada Subject: SPARK X-Priority: 3 X-MSMail-Priority: Normal X-Newsreader: Microsoft Outlook Express 5.50.4133.2400 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4133.2400 Message-ID: Date: Mon, 06 Aug 2001 16:49:56 GMT NNTP-Posting-Host: 24.188.177.13 X-Trace: news02.optonline.net 997116596 24.188.177.13 (Mon, 06 Aug 2001 12:49:56 EDT) NNTP-Posting-Date: Mon, 06 Aug 2001 12:49:56 EDT Organization: Optimum Online Xref: archiver1.google.com comp.lang.ada:11394 Date: 2001-08-06T16:49:56+00:00 List-Id: I have been to various web sites like www.sparkada.com in an effort to research the SPARK language. Is SPARK Examiner the only SPARK language tool available? What is the cost? Are there any open source alternatives? I am fascinated by the concept of verifying correctness completely at compiler/pre-compile time. Answers to my questions and any additional information would be greatly appreciated. Thanks.