Ada

From Openproofs

Jump to: navigation, search

Ada programs can be compiled by a FLOSS compiler, GNAT, which is integrated into the gcc compiler suite. Ada Core Technologies offers support for GNAT.

SPARK is a sub+superset of Ada for developing provable programs. Programs written in SPARK can be compiled by a standard Ada compiler, including GNAT (GPL). They can also be processed by SPARK tools developed by Praxis that were released as open source software (GPL license) in June 2009.

Retrieved from "http://www.openproofs.org/wiki/Ada"