Czy jest jakieś narzędzie do prototypowania semantyki języka programowania i systemu typów, a także umożliwia pewnego rodzaju sprawdzanie modelu standardowych właściwości, takich jak poprawność typu?
Pytam o to, ponieważ czytam książkę o stopie i zapewnia on dokładnie taką funkcjonalność, jakiej chcę, ale dla modeli wyrażonych za pomocą logiki relacyjnej.
Zdaję sobie sprawę z Ott , ale nie ma takiej możliwości „sprawdzania modelu”, ponieważ koncentruje się na generowaniu kodu dla systemów asystenta dowodu.
Wszelkie odniesienia do takiego istnienia narzędzi byłyby fajne.
1
Ott jest krokiem pierwszym, a następnie sprawdzasz model w swoim ulubionym asystencie dowodu.
—
Gilles „SO- przestań być zły”
@Gilles: Ok, ale punktem narzędzia do sprawdzania modelu jest to, że generuje cały zestaw elementów o danym rozmiarze w celu sprawdzenia, czy właściwość jest dla nich rzeczywiście ważna. W ten sposób będę musiał zakodować tę część generacji dla każdego zdefiniowanego języka. Czy wiesz, czy jest jakiś sposób na zautomatyzowanie tego etapu generacji?
—
Rodrigo Ribeiro
Technicznie możesz to zrobić w asystencie dowodu (przynajmniej w jednym z takich jak Coq), ale prawdopodobnie będzie to bardzo powolne. Proof asystenci nastawieni są na dowody wspierane przez ludzi, zamiast automatycznie wypróbowywać miliony sposobów rozwiązania problemu. Jeśli chcesz ponownie użyć Ott, możesz dodać backend do swojego ulubionego modelu sprawdzania.
—
Gilles „SO- przestań być zły”