CafeOBJ
CafeOBJ — одна з мов OBJ-родини декларативних мов програмування ультра високого рівня. Є найбільш передовою мовою формальної специфікації, яка успадкувала багато додаткових можливостей (наприклад, гнучке мікс-виправлення синтаксису, потужна і зрозуміла система введення і так далі) від OBJ алгебраїчної мови специфікації.
CafeOBJ це мова для написання формальних (наприклад, математичних) специфікацій моделей для широкого різноманіття програмного забезпечення і систем, і верифікації їх властивостей. CafeOBJ реалізується логікою загальної алгебри (англ. equational logic), шляхом переписування і може бути використана як потужна інтерактивна система доведення теорем. Сувора логічна семантика, що базується на інструкціях.
Іншими важливими мовами з OBJ-родини є Eqlog, FOOPS, Kumo, Maude і OBJ3.
Може бути завантажена тут [Архівовано 17 жовтня 2012 у Wayback Machine.].
Див. також[ред. | ред. код]
Посилання[ред. | ред. код]
- Офіційний сайт CafeOBJ [Архівовано 6 лютого 2016 у Wayback Machine.] (англ.)
- The OBJ family [Архівовано 27 травня 2009 у Wayback Machine.] (англ.)
- Verifying Specifications with Proof Scores in CafeOBJ, Kokichi Futatsugi, YouTube (англ.)
|
Це незавершена стаття про мови програмування. Ви можете допомогти проєкту, виправивши або дописавши її. |
 | Ця стаття не має інтервікі-посилань. |