https://en.wikipedia.org/wiki/SPARK_(programming_language)
Мне непонятно, какая программа является компилятором в SPARK 2014 GPL edition.
Исходя из того, что spark - это подмножество ada, то та же самая?
Т.е. я пишу в расширенном синтаксисе (кстати, где про него прочитать?), а потом собираю как обычно?
GNATprove - это доказыватель, они так и пишут, что:
- the GNAT compiler toolchain
- the SPARK Ada verification and prover toolset
- the GNAT Programming Studio IDE
Какие книги читать про доказывание в этой системе?
UPD: http://alfa.di.uminho.pt/~edbrito/EVTSIC2010.pdf - A (Very) Short Introduction to SPARK