Vi beskriver en algoritm för att bestämma den första ordningens multisorterade teori BAPA, som kombinerar Booleska algebras av uppsättningar av otolkade element (BA) och Presburger aritmetiska operationer (PA). BAPA kan uttrycka förhållandet mellan heltalsvariabler och kardinaliteter av obundna finita uppsättningar, och det stöder godtycklig kvantifiering över uppsättningar och heltal. Vår motivation för BAPA är att bestämma verifieringsförhållanden som uppstår i den statiska analysen av datastrukturkonsistensegenskaper. Datastrukturer använder ofta ett heltalsvariabel för att hålla reda på antalet element de lagrar; en invariant av en sådan datastruktur är att värdet av heltalsvariabeln är lika med antalet element som lagras i datastrukturen. När innehållet i datastrukturen representeras av en uppsättning kan de resulterande begränsningarna fångas upp i BAPA. BAPA-formler med kvantifieralternationer uppstår vid verifiering av program med annoteringar som innehåller kvantifieringar eller vid bevisande av simuleringsförhållandeförhållanden för förfining och likvärdighet av programfragment. Dessutom kan BAPA begränsningar användas för att bevisa avslutandet av program som manipulerar datastrukturer, liksom i begränsning databas frågebedömning och loop invariant inference. Vi ger en formell beskrivning av en algoritm för att bestämma BAPA. Vi analyserar vår algoritm och visar att den har optimal alternerande tid komplexitet och att komplexiteten i BAPA matchar komplexiteten i PA. Eftersom det fungerar genom en minskning till PA, vår algoritm ger decidability av en kombination av uppsättningar av otolkade element med någon decidable förlängning av PA. När den är begränsad till BA-formler kan algoritmen användas för att bestämma BA i optimal alternerande tid. Dessutom kan algoritmen eliminera enskilda kvantifier från en formel med fria variabler och därför utföra projektion på en önskvärd uppsättning variabler. Vi har implementerat vår algoritm och använt den för att skriva ut verifierings villkor i Jahob systemet för datastruktur konsekvens kontroll av Java program; vår erfarenhet tyder på att en enkel implementering av algoritmen är effektiv på icke-triviala formler så länge antalet inställda variabler är liten. Vi rapporterar också om en ny algoritm för att lösa det kvantifierfria fragmentet av BAPA.
Det kvantifierade fallets komplexitet och det första genomförandet av kvantifieringsmetoden beskrivs i Ref.
Deciding Boolean Algebra with Presburger Arithmetic
{'venue': 'Journal of Automated Reasoning', 'journal': 'Journal of Automated Reasoning', 'mag_field_of_study': ['Mathematics', 'Computer Science']}