Vi utvecklar grunden för den visningsbaserade specifikationen av programvaruartefakter i första ordningens logik. Standardbegrepp av modeller och semantik av första ordningens logik generaliseras till partiella modeller som inte har tillgång till hela den globala signaturen. På modellteoretisk nivå uppnås detta via Smyths maktdomän över elementens semantiska universum. På den logiska nivån uppnår vi detta via Smyth powerdomain över de vanliga tvåvärderade booleanerna. Ett förfiningsbegrepp utvecklas och dess sundhet bevisas för en fast uppsättning semantiska element. Standardmodeller och semantik av första ordningens logik subsumeras av vårt ramverk som modeller där all signaturinformation är närvarande ("fullständiga modeller"). Vi nedbryter våra semantik till ett samförstånd (unionen av Smyth powerdomain) av en optimistisk och en pessimistisk semantik. På så sätt kan vi beräkna denna semantik som en standard modellkontroll i första ordningens logik över en modell som lyfts av Smyth powerdomain.
Grunder för visningsbaserad modellkontroll, där modeller är av första ordningens logik med transitiv stängning, utvecklas i REF.
Model-Checking View-Based Partial Specifications
{'venue': 'MFPS', 'journal': 'Electr. Notes Theor. Comput. Sci.', 'mag_field_of_study': ['Computer Science']}