Marek Sawerwain: CafeOBJ – maszynowy system dowodzenia
![Programista 03/2018 (70) kwiecień/maj [okładka]](https://programistamag.pl/wp-content/uploads/magazines/covers/70.jpg)
CafeOBJ to specjalny język programowania przeznaczony do tworzenia formalnych i zarazem matematycznych specyfikacji modeli opisujących różnego typu systemy z otaczającego nas świata. Zarówno tego prawdziwego, ale także wirtualnego. A w szczególności za pomocą CafeOBJ możemy opisywać tworzone przez nas programy. O CafeOBJ można też powiedzieć, iż jest to system wspomagający przeprowadzanie dowodów matematycznych dla systemów formalnych. Inaczej mówiąc, możemy przeprowadzić weryfikację, czy badany system spełnia postawione przez nas założenia. Lecz zamiast pracować z kartką i ołówkiem, CafeOBJ przeprowadzi dowód matematyczny za nas.