Sprawdzanie modelu abstrakcyjnego

W informatyce i matematyce sprawdzanie modelu abstrakcji dotyczy systemów, w których rzeczywista reprezentacja jest zbyt złożona przy opracowywaniu samego modelu . Projekt przechodzi więc swoistą translację do pomniejszonej wersji „abstrakcyjnej”.

Zbiór zmiennych jest podzielony na widoczne i niewidoczne w zależności od zmiany ich wartości. Rzeczywista przestrzeń stanów jest podsumowana w mniejszym zestawie widocznych.

Galois podłączony

Rzeczywiste i abstrakcyjne przestrzenie stanów są Galois połączone . Oznacza to, że jeśli weźmiemy element z przestrzeni abstrakcyjnej, skonkretyzujemy go i wyabstrahujemy skonkretyzowaną wersję, wynik będzie równy oryginałowi. Z drugiej strony, jeśli wybierzesz element z rzeczywistej przestrzeni, wyabstrahujesz go i skonkretyzujesz wersję abstrakcyjną, ostatecznym rezultatem będzie superzbiór oryginału.

To jest,

${\ Displaystyle \ eta}$ ( ${\ Displaystyle \ teta}$ (abstrakcyjny)} = abstrakcyjny ${\ Displaystyle \ teta}$ ( ${\ Displaystyle \ eta}$ (rzeczywisty)) ${\ Displaystyle \ supseteq}$ prawdziwy

Zobacz też

• Interpretacja abstrakcyjna
• Zautomatyzowane dowodzenie twierdzeń
• Logika drzewa obliczeniowego
• Weryfikacja formalna
• Lista narzędzi do sprawdzania modeli
• Analiza programu (informatyka)
• Statyczna analiza kodu

•   Edmund M. Clarke i Orna Grumberg i David E. Long (1994). „Sprawdzanie modeli i abstrakcja”. Transakcje ACM dotyczące języków i systemów programowania . 16 (5): 1512–1542. CiteSeerX 10.1.1.79.3022 . doi : 10.1145/186025.186051 .