Abstrakt. Denna artikel presenterar den systematiska utformningen av en klass av relationella numeriska abstrakta domäner från icke-relationella. Konstruerade domäner representerar uppsättningar av invarianter av formen (vj − vi  på C), där vj och vi är två variabler, och C lever i en abstraktion av P(Z), P(Q), eller P(R). Vi kommer att kalla denna familj av domäner svagt relationsdomäner. Det underliggande konceptet tillåter denna konstruktion är en förlängning av potentiella grafer och kortaste vägen stängning algoritmer i exotisk-liknande algebras. Exempel på konstruktioner ges för att hämta välkända domäner såväl som nya. Sådana domäner kan sedan användas inom ramen för Abstract Interpretation för att utforma olika statiska analyser. En stor fördel med denna konstruktion är dess modularitet, vilket gör det möjligt att snabbt genomföra nya abstrakta domäner från befintliga. Att bevisa att ett program är korrekt är viktigt, särskilt för kritiska och inbyggda tillämpningar (såsom flygplan, raketer och så vidare). Bland flera korrekthetskriterier, bör man se till att ett program aldrig kan utföra en körning-tid fel (dela med noll, överflöd, etc.). En klassisk metod består i att hitta en säkerhetsinvariant före varje farlig operation i programmet, och kontrollera att invarianten innebär det goda beteendet i den efterföljande operationen. Eftersom denna uppgift ska utföras på hela programmet-innehålla kanske tiotusentals rader-och måste upprepas efter även den minsta kodändring, vi behöver en rent automatisk statisk analys metod. Att upptäcka de snävaste invarianterna av ett program kan inte helt mekaniseras i allmänhet, så vi måste hitta någon form av ljud approximation. Med ljud menar vi att analysen bör finna en över- approximation av den verkliga invarianten. Vi kommer alltid att upptäcka alla buggar i ett program. Men vi kanske hittar falska larm. Detta arbete stöddes delvis av FoTU-projektet IST-1999-20527 "DAEDALUS" inom det europeiska IST-FP5-programmet. Vi kommer att arbeta i den välkända Abstract Interpretation ram, som föreslagits av Cousot och Cousot i [6, 7], vilket gör att vi enkelt kan beskriva ljud och beräkningsbara semantik approximationer. Metodens kärna är att utforma en så kallad abstrakt domän, det vill säga en praktisk representation av de invarianter vi vill studera, tillsammans med en fast uppsättning operatörer och överföringsfunktioner (union, skärningspunkt, breddning, uppdrag, vakt osv.) används för att efterlikna semantiken i programmeringsspråket. Vi kommer att överväga här numeriska abstrakta domäner. Med tanke på den uppsättning V av de numeriska variablerna i ett program med värde i uppsättningen I (som kan vara Z, Q eller R), en numerisk abstrakt domän kommer att representera och manipulera undergrupper av V → I. Icke-relationella domäner är snabba, men lider av dålig precision: de kan inte koda relationer mellan variabler i ett program. Relationella domäner är mycket mer exakta, men också mycket kostsamma. Tänk till exempel på det enkla programmet i figur 1 som simulerar många slumpmässiga promenader och lagrar träffarna i en uppsättning. Vårt mål är att upptäcka att x vid programpunkt (•) är i uppsättningen {−5, −3, −1, 1, 3, 5} av tillåtna index för träff, så att instruktionen hit[x]++ är korrekt. De invarianter som finns vid (•) med flera metoder visas i figur 2. Observera att även om den önskade invarianten är en enkel kombination av ett intervall och en kongruenssamband, alla icke-relationella analyser misslyckas att upptäcka det eftersom de inte kan härleda förhållandet mellan x och i vid programpunkt (.). Det är ofta så att man, för att hitta en given invariant i slutet av en slinga, måste kunna uttrycka invarianter av en mer komplex form inuti slingan. I detta exempel kan önskat resultat erhållas genom att använda relationsanalyser, som visas i figur 2. Pratt påpekade i [26] att tillfredsställandet av en uppsättning begränsningar av formen (x − y ≤ c) kan testas effektivt i Z, Q, eller R genom att titta på de enkla slingorna i en riktad viktad graf-så-kallade potentiella graf. Shostak utvidgades sedan i [27] denna grafbaserade algoritm till att vara tillfredsställande för begränsningar i formen (αx + βy ≤ c), i Q eller R. Harvey och Stuckey visade [17] att Shostaks algoritm kan användas för att kontrollera tillfredsställandet av begränsningar i formen (±x ± y ≤ c) i Z. Dessa strategier fokuserar endast på tillfredsställelse och tar inte itu med problemet med manipulerande begränsningar uppsättningar. hit: array {-5,-3,-1,3,5} → int; för k=1 till 1000 do x=0; Polyhedron Congruence equality Med Pratts anmärkning utvecklade modellkontrollgemenskapen en struktur som kallas Difference-Bound Matrix (DBM, för kort) och algoritmer baserade på kortaste vägen stängning av viktade grafer för att representera och manipulera begränsningar av formen (x − y ≤ c) och (x ≤ c). DBM används för modellkontroll av timd-automata. I [28], Toman och Chomicki introducerade periodicitet diagram som manipulera begränsningar av formen (x  på y + c [k]), och tillämpa detta för att begränsa logik programmering och databas fråga. Till skillnad från modellkontroll och begränsning programmering, skulle vi vilja analysera generiska program, och inte bara system stängda under begränsade begränsningar former-såsom timed automata, eller databas frågespråk. Vår metod är först att välja en oföränderlig form, och sedan att utforma en fullfjädrad abstrakt domän (inklusive vakt- och uppdragsöverföringsfunktioner, samt en bredare operatör) som gör det möjligt att upptäcka invarianter av denna form på något program, med hjälp av kanske grova över- approximationer för de semantiska funktioner som inte kan representeras exakt med hjälp av den valda invarianta formen. I [23] har vi redan presenterat en DBM-baserad abstrakt domän som gör det möjligt att upptäcka invarianter av formen (x− y ≤ c) och (x ≤ c). Under [24] presenterade vi en liten förlängning, kallad oktagon abstrakt domän, som gör det möjligt att upptäcka invarianter av formen (±x ± y ≤ c). Vårt mål är att föreslå en ny familj av numeriska abstrakta domäner, baserade på kortaste-väg stängningsalgoritmer, som gör det möjligt att upptäcka invarianter av formen (x-y  på C), där C bor i en icke-relationell domän. Denna familj generaliserar DBM-baserade abstrakta domänen [23] och låter oss bygga nya domäner, såsom zonkongruensdomänen som upptäcker invarianter av formen (x  på y + c [k]). Sådana relationsdomäner är mellan, i termer av kostnad och precision, icke-relationella domäner och klassiska relationsdomäner-såsom polyhedron eller kongruensjämlikhet. Således kommer vi att kalla dessa domäner svagt relationsdomäner. Vi hävdar att sådana domäner är användbara som de ger, på exemplet Figur Papperet är organiserat enligt följande. Avsnitt 3 omformulerar uppbyggnaden av icke-relationella numeriska abstrakta domäner genom att använda grundbegreppet. Avsnitt 4 förklarar vår allmänna konstruktion av svaga relationsdomäner och tillämpar den för att hämta zondomänen och bygga nya abstrakta domäner. I avsnitt 5 ges några tillämpningar och idéer till förbättringar. Vi avslutar i avsnitt 6. Viktiga bevis skjuts upp till bilagan. Att läsa dem kan bidra till att förstå de definitioner som valts i avsnitt 3-4 (huvudsakligen hypoteser 1). I detta avsnitt erinras först om begreppet numerisk abstrakt domän. Vi introducerar det nya grundbegreppet och visar hur det kan användas för att hämta standard icke-relationella domäner. Att införa ett sådant begrepp endast för detta ändamål skulle vara formalism för formalismens skull. I nästa avsnitt kommer vi dock att visa hur man använder detta koncept för att bygga våra svaga relationsdomäner. Därför är baser den gemensamma nämnaren mellan klassiska icke-relationella domäner och vår svagt relationella domänfamilj. Ur genomförandesynpunkt är baser moduler som delar en gemensam signatur, och vi föreslår en functor för att bygga icke-relationella domäner från denna signatur, och en functor för att bygga svagt relationsdomäner. Ur matematisk synvinkel gör detta tillvägagångssätt våra bevis modulära och lättare att hantera. Låt P vara ett förfarande-fri, pekarfri program såsom den i Figur 1. Låt V = {v 0,. ., v N −1 } vara den uppsättning av dess numeriska variabler, med värden i uppsättningen I (som kan vara Z, Q, eller R). Vi bifogar till varje nod av kontrollflödesgrafen över P en uppsättning miljöer e  på ett sätt som motsvarar dess värde. Informationen sprids med hjälp av följande ekvationer: • vakter, som motsvarar tester i det ursprungliga programmet, filtrera miljön: e • uppdrag ändra värdet på en variabel: e • facket samlar miljöer vid styrflödet ansluter. På grund av loopkonstruktioner innehåller styrflödesgrafen loopar och ekvationssystemet som beskrivs ovan är rekursivt. Klassisk säkerhetssemantik är den minsta fixpunktslösningen. Denna semantik är inte decimerbar i allmänhet. Man konstruerar på så sätt en abstrakt domän [6] som är en dator-representabel delvis beställd uppsättning (D, ) ansluten till (D,  på) av en monoton konkretisering funktion Ε. Vakt, uppdrag, och fackliga operatörer har ljud över approximationer i D, det vill säga: Till skillnad från klassisk data-flödesanalys, D kan ha en oändlig höjd, så man behöver en bredare operatör [6] för att beräkna, i ändlig tid, en över approximation av minst fixpoints. Den expanderande operatören bör ha följande egenskaper [6]: Definition 1. Bredare. 1. Vad är det för fel på dig? C, x x y och y x y. Den minsta fixeringspunkten för en abstrakt operatör F ersätts av gränsen för den stationära sekvensen för mer information om när och hur man använder breddningar. Det är ett viktigt resultat av den abstrakta tolkningen att man, när man i den abstrakta domänen med vidgar sig, i ändlig tid får en överskattning av de första semantikerna. Vi kallar grunden för en struktur som representerar och manipulerar undergrupper av I på ett sätt som lämpar sig för att bygga en icke-relationell abstrakt domän. Sådana baser kommer sedan att användas i följande avsnitt för att bygga vår familj av relationsdomäner. Den ges av: Definition 2. Utgångspunkt. 1. Vad är det för fel på dig? En dator-representabel uppsättning C med partiell ordning  på och minst element  på. Det finns en över- approximation  på skärningspunkten:. Om C har strikt oändliga kedjor, det finns en växande operatör. ♦ Genom stränghet, γ( ska) = ∅. Tack vare punkterna 2 och 3 finns det ett unikt abstrakt element  på ett sådant sätt att γ( ska) = I. Den minst övre gränsen är också en över- approximation för unionen: Vi presenterar nu några uppsättningar baser som gör att vi kan hämta den icke-relationella konstant utbredning [6], intervall [5], och kongruens domäner [14]. Alla abstrakta operatörer är enkla och diskuteras inte här (se [6] för mer information). Det finns inget behov av en allt större operatör. De flesta abstrakta operatörer är enkla (se [5] för mer information). Vi kommer bara att minnas här den klassiska breddning operatör: I Q eller R kan man alternativt definiera det öppna intervallet lattice C ]a,b[ på samma sätt. Man kan till och med kombinera dessa uppgifter för att få en grund C [a,b] [där varje gräns får eller inte får ingå. En bas bygger på C Z AZ+b tack vare de operatörer som beskrivs i figur 4 (med hjälp av definitionerna i figur 3). För koncishetens skull uppvisar figur 4 emellertid inte abstrakta k-ary aritmetiska uttryck, utan det binära plustecknet, som betecknas av infix-operatören (se [14] för mer information). Det finns ingen strikt ökande oändlig kedja, så det finns inget behov av en växande operatör. Man kan också överväga att anpassa definitionerna i figurerna 3 och 4 till rationella kongruenser [16]: 1 Gränser är en del av intervallet endast om det är ändligt. Förväxla inte med slutna intervallangivelser såsom [a, +∞]; intervallet kan inte innehålla oändliga element. I följande, x, x ′  på Z och y, y ′ på N *  på {∞}: Bygga en icke-relationell domän (D, ) från en grund (C,  på) är enkel: • Konkretiseringen â, ordning, union  på och breddning av är helt enkelt punktvisa versioner av motsvarande operatörer på grundval. • Uppdrag definieras med hjälp av den abstrakta motsvarigheten till uttryck: I andra vaktfall är det säkert att använda identitetsfunktionen. Ur ett genomförandeperspektiv är den icke-relationella domänen helt enkelt en allmän functor-modul, och varje basimplementation är en modul. Nu skulle vi vilja representera relationer av formen v j − v i  ska γ(C) där C bor i en bas C (i stället för v i  ska γ(C)). En tydlig grund är inte tillräcklig, vi kommer att behöva ett sätt-en så kallad stängning-att sprida relationsinformation. Huvudresultatet av detta dokument kan schemaläggas enligt följande: bas (med ytterligare hypoteser) + stängning = en svag relationsdomän Inte alla baser C är godtagbara. Vi behöver följande ytterligare hypoteser: Hypoteser 1. Godtagbara baser. 1. Vad är det för fel på dig? Det finns exakta abstrakta motsvarigheter för skärningspunkten  ska (som också bör vara en lägre gräns för  till), unary minus  på, och binära plus  på operatörer: (Abstrakt skärningspunkt.) • Konkretisering: • Intersektion (exakt abstrakt motsvarighet till skärningspunkten): • Minsta övre gräns: • Summa (exakt abstrakt motsvarighet för binär + operatör): 5. på distribuerar  på och  på. De är pendlings- och associativa. Dessa hypoteser angavs för att bevisa vårt huvudsakliga tema, vilket är riktigheten hos stängningsoperatören. Således kan man behöva vänta tills Theorem 6-och dess bevis uppskjutits i bilaga A-Anmärkning att Hypoteser 1.3-4 är mycket starka. Den fullständiga grunden C = P(I), till exempel, respekterar dem inte. Anmärkning. Det finns likheter mellan baser med avseende på hypoteser 1 och grafteorins klassiska begrepp om fullständig dïoid [13]-en utvidgning av exotiska algebror. En komplett dïoid är en komplett semi-lattice med ett tillägg (våra) och en multiplikation (våra) som distribuerar över tillägget. Men full distributivitet i dïoider innebär att  på ett sådant sätt att vi skulle ha föredragit  på ett sådant sätt att vi skulle ha gjort det. Inom vår ram är därför distribuiviteten begränsad (Hypothesis 1.4). En uppsättning begränsningar i formuläret v j − v i  till γ(C), C  till C representeras nu av en sammanhängande begränsningsmatris : Definition 3. Restriktiva matriser. 1. Vad är det för fel på dig? En begränsningsmatris m är en N × N-matris med grundämnen i C; grundämnet m ij representerar begränsningen v j − v i  till γ(m ij ). Vår abstrakta domän är den uppsättning D av sammanhängande begränsningar matriser, beställd av den punktvisa förlängningen av den partiella ordningen på C: Konkretiseringsfunktionen på D är Ε, och vi har: Men, detta är inte en motsvarighet och vi kan ha två olika begränsningar matriser m  och = n med samma concretization ρ (m) = Γ (n). Implicit Restriktioner. Eftersom vår abstrakta domän är relationell är begränsningarna mellan variablerna inte oberoende. Man kan härleda en begränsning på x − z genom att lägga till en begränsning på x − y till en begränsning på y − z. Sådana härledda begränsningar kallas implicita begränsningar eftersom de inte kan vara närvarande explicit i m. Mer allmänt, med tanke på någon väg i = i 1,. .., i n = j i m, kan vi konstruera följande implicita begränsning: Floyd-Warshall algoritmen valdes eftersom det är lätt att förstå, enkelt att genomföra och lätt att anpassa till begränsning matriser. Den utför O(N 3 ) elementära basoperationer. Här är huvudteoremet i den här tidningen. Följande resultat kommer att användas i stor utsträckning i avsnitt 4.4 för att utforma abstrakta operatörer. Beviset för detta teorem är starkt beroende av Hypoteser 1-i själva verket, beviset i sig motiverade hypoteserna. Teorin 6. Stängning. har följande egenskaper: Vi kan enkelt anpassa algoritm-permuterande variabler-för att få en allmän inkrementell stängningsalgoritm som utför O(N 2 · c) elementära basoperationer, där c är antalet linjer och kolumner som har ändrats sedan den senaste stängningen. Tålamodstestning. Test av tillfredsställandet av en begränsningsmatris görs med hjälp av Theorem 6.2. Till skillnad från begränsning programmering metod, använder vi inte en specifik loop-baserad tillfredsställande algoritm, men låt vår generiska stängningsalgoritm lösa både tillfredsställande och normala form problem på en gång. Jämlikhet, integrationstestning. Den normala formen egenskap av Theorem 6.3 gör det möjligt för oss att enkelt testa jämlikhet och inkludering av icke-tomma concretizations: Theorem 7. Testning av jämställdhet och integration. 1. Vad är det för fel på dig? Observera att vi inte behöver avsluta rätt argument när vi testar inkludering. Fackförening, intersektion. γ(C) är stabil under skärningspunkten, så vi helt enkelt sträcka punkt-wisely  på att representera skärningspunkten mellan två concretizations: Om  till är en minst övre gräns, på kan användas för att bestämma den minst övre gränsen av två concretizations, förutsatt att argumenten är stängda matriser. Bredare. D har oändliga strikt ökande kedjor endast om C har. En breddning på D erhålls genom punktvis tillämpning av den vidgade metoden på C:  med respekt för definition 1. Således kan den minsta fixpunkt för en operatör F överskattas av gränsen för den stationära sekvensen X i+1 = X i på F (X i ). Man kan förvänta sig, som för den minst övre gränsen, att få en bättre precision genom att avsluta argumenten i, Men så är inte fallet. Ännu värre, Verkställer stängningen av kedjan genom att dator X i+1 = (X i på F (X i ))  och bryter den stigande kedjan tillstånd och förhindrar analysen från att avslutas i vissa fall. Vi förespråkar här användningen av följande iteration: Vakt. Vi kan enkelt genomföra tester av formuläret (v j − v i  på C?): Tester av blanketten (v j  på C?) implementeras genom att välja i = 0. För andra tester, är det säkert att göra ingenting: Projektion. För att hitta den uppsättning värden som en variabel kan ta, använder vi följande teorem som härrör från mättnad egenskapen hos stängningen: Glöm. Att glömma värdet av en variabel är användbart för att genomföra den slumpmässiga uppgiften (v i ←?), som också fungerar som en grov approximation för komplexa uppdrag. Innan man glömmer all information om en variabel, bör man stänga argumentmatrisen så att vi inte förlorar implicita begränsningar: Uppdrag. För inlämning av blanketten (v i ← v j + c) kan man hitta en exakt abstrakt motsvarighet: För generiska uppdrag (v i ← expr(v 1,. .., v N −1 ) ), kan man alltid falla tillbaka för att oprecis icke-relationell analys, först projicera variablerna, sedan använda abstraktion expr  på expr i vår grund: ). Att försöka vara den mest exakta i alla fall kan leda till komplexa algoritmer. Det verkar bara värt att försöka vara lite mer exakt i vissa utbredda fall, såsom (v i ← v j + v k ), till exempel: Interaktion med stängningen. Vissa av de ovan nämnda operatörerna kräver att matrisargumentet(erna) stängs. Vissa respekterar stängning-resultatet avslutas om argumenten är (är)-och vissa inte (intersektion, vakt, uppdrag, etc.). Vi förespråkar därför användningen av en lat metod som kommer ihåg när en matris är i sluten form, och återberäknar stängningen endast när det behövs. När bara ett fåtal rader och kolumner i matrisen ändras (vakt, uppdrag, etc.).), kan vi använda den stegvisa stängning. Det är meningslöst när alla koefficienter ändras på en gång (intersektion, breddning). Vi är nu redo att tillämpa vår konstruktion på de baser som presenteras i Avsnitt 3.3, tack vare följande teorem: Jämfört med klassiska DBMs [23], är den domän som erhålls lite överflödig (varje begränsning representeras två gånger), men har exakt samma uttrycksfullhet och komplexitet. Den har fördelen att den genomförs över alla befintliga intervallbibliotek, vilket i hög grad minskar behovet av programmering. Man kan också förbättra zondomänen i Q och R med hjälp av C ] [a,b] [grund som manipulerar både strikta och icke strikta begränsningar. Zon-Congruence-domänen. Med hjälp av heltal kongruens bas C Z AZ+b, bygger man en domän som upptäcker begränsningar i formen ). Denna konstruktion ser ut som periodicitetsdiagram [28], men vi behandlar här fallet med minst övre bundna och allmänna överföringsfunktioner i detalj, medan [28] endast är intresserad av tillfredsställelse, normal form och förening. Dessutom anser vi att [28] saknar det korrekta beviset på den normala formen teorem (vår sats 6) och inte förstår att den förlitar sig på vissa starka egenskaper kongruensuppsättningar (Hypotes 1). Vårt ramverk kan också utvidga denna domän till ett område med rationella kongruenser: Product Domain. Reducerad produkt är en välkänd teknik [6] för att förbättra precisionen i en analys genom att kombinera kraften i två abstrakta domäner. Det ger ofta bättre resultat än två separata analyser, eftersom det förmedlar information från en domän till en annan under analysen via en så kallad minskning förfarande, som är ett par binära operatörer (, ) sådan att: I vårt fall kan minskningen definieras på baser-så länge Hypoteser 1 inte bryts-med exakt samma precision fördel. Minskningar är dessutom lättare att utforma på icke-relationsbaser. Till exempel, om vi använder följande minskning mellan C [a,b] och C Z AZ+b, vi få en grund som tillåter byggandet av en domän för begränsningar av formen misslyckande. Hittills verkar allt fungera bra. Man kan dock hitta vissa grunder som används inom mycket vanliga abstrakta områden som inte respekterar hypoteser 1. Till exempel, teckenbasen ) inte respekterar Hypotes 1.1 (den är inte stabil under skärningspunkten). Vi vet inte om det är möjligt att bygga svaga relationsdomäner från sådana baser. Varaktighet. När det gäller icke-relationella domäner, den svagt relationella domän familjen är helt enkelt en generisk modul functor, med samma baser implementation moduler som parameter. Ansökningar. Hittills har detta ramverk bara implementerats som en OCaml-prototyp och testats på några exempel på leksaker. Vid programpunkt (•) av programmet i Figur 1, den reducerade produkten av zonen och zon-kongruens domäner hittade invariant (x ≤ 5, x 1 [2]), som är nästan lika bra som polyhedron och kongruensjämlikhet analyser kombinerade (Figur 2). Den upptäckte inte att (x ≥ −5), men den abstrakta oktagondomänen för [24] som också använder grafbaserade algoritmer kan göra det. Om konstanten 5 i programmet i figur 1 ersätts med en variabel m vars värde inte är känt vid analystidpunkten, finner analysatorn fortfarande den exakta skalbarheten. Det är fortfarande okänt om grafbaserade abstrakta domäner skalar upp sig. På grund av kostnaden för det kvadratiska minnet kan det inte hantera alla variabler i ett stort program på en gång; man måste dela upp denna uppsättning i paket där relationsinformation kan vara viktig. Dessa paket behöver inte delas, och man kan använda pivotvariabler för att överföra information mellan paket. Vi undersöker för närvarande sådana metoder. Eftersom vår domänfamilj är relationell anpassas den också till symboliska och modulära analyser. Man kan skära ner kostnaden för en analys och göra det inkrementell genom att analysera separat små bitar av ett program [8]. Teoretiska tillägg. I den här artikeln försökte vi förena en grafbaserad numerisk satisfiability-algoritm och utvidga den till en abstrakt domän, i en enhetlig ram. Här hanteras dock inte några grafbaserade algoritmer: den abstrakta oktagondomänen [24] (±x ± y ≤ c begränsningar) och Shostaks satisfiabilityalgoritmer [27] (αx + βy ≤ c). Det skulle vara intressant att förena alla dem i en allmän ram och härleda en numerisk abstrakt domän för begränsningar av formen (αx + βy ≤ c). I detta dokument har vi föreslagit en systematisk uppbyggnad av en familj av relationsdomäner som representerar och manipulerar begränsningar av formen (x-y  på C). Denna konstruktion kan ses som en functor lyft icke-relationella domäner till relationella. Minneskostnaden för ett abstrakt tillstånd är kvadratisk, och varje överföringsfunktionsapplikation utför, på värre sätt, ett kubiskt antal operationer i den icke-relationella domänen. Metodens crux är anpassning av den kortaste vägen stängningsalgoritmen till en normal form, vilket gör det möjligt att härleda de flesta abstrakta operatörer och överföringsfunktioner. Inom denna ram har vi framgångsrikt hämtat den befintliga DBM-domänen och konstruerat nya. Det är författarens uppfattning att dessa domäner fyller en precisions- och komplexitetsklyfta mellan tidigare icke-relationella och relationella domäner, och kan användas för att utforma medelstora, men ändå exakta analyser. Erkännanden. Vi vill tacka P. Cousot, J. Feret, X. Rival, och C. Hymans, liksom anonyma domare, för deras användbara kommentarer.  Referenser Vi presenterar här det fullständiga beviset på huvudteorin, Theorem 6. Det är beviset på detta teorem som motiverade valet av Hypoteser 1. Observera att beviset på detta teorem är mycket enklare i specialfallet av intervallbasen C [a,b] (se Theorem 2 i författarens masteruppsats [22] ). Notera också att en del av detta teorem för kongruensmålet C Z AZ+b diskuteras av Toman och Chomicki i [28], men beviset är något utspritt (Lemma 2.12). Våra bevis bygger starkt på det faktum att C Z AZ+b verifierar Hypotes 1.3, vilket inte är trivialt. • Påståenden: Vi har bevis, i, j, m • Bevis. Anta att m är sammanhängande. Vi bevisar först att det motsäger det faktum att ρ (m) = ∅ på grund av den inledande punkten. • Lemma 1: för alla fasta 0 ≤ i, j ≤ N − 1, 0 ≤ k ≤ N, och sökväg i = i 1,. .., i n = j i m så att i l < k för 1 < l < n, och i s = i t för 1 < s < t < n, vi har m Corollary. Genom att tillämpa denna lemma med k = N får vi: för alla enkla bevis. Genom upprepning. Egenskapen är uppenbar för k = 0 eftersom det motsvarar m 0 ij m ij och vi har m 0 = m. Antag att egenskapen är sant för en k < N och låt i = i 1,. .., i n = j vara en väg som uppfyller hypoteserna i lemma för k+1. Om "l" {2,..., n − 1}, i l < k, är egenskapen sann genom återfallshypotes och eftersom m k+1 ij m k ij. Tvärtom, om det finns en l sådan att i l ≥ k, vi vet att det är unikt och att vi får det förväntade resultatet genom att tillämpa återfall hypotes till i = i 1,. .., i l = k i m k ik, och k = i l,. .., i n = j i m kkj, och med hjälp av associativitet av  på. • Lemma 2: om, för några 0 ≤ i, j < N, För alla vägar i = i 1,. .., i n = j, vi har... {1,.., n − 1},, som inte är tom. • Lemma 3: Sammanfallande. När vi sätter k = N i lemma, får vi i, j, bevis. Genom upprepning. Om k = 0, då har vi m ij... m 0 ij eftersom m 0 = m, så ett fortiori lemma är sant. Antag att fastigheten är sant för k < N. För att bevisa egendomen för k + 1, vi behöver bara bevisa att, Vi anser bara uppsättningen av vägar från i till j som passerar genom variabel k: Den sista jämlikheten kommer från Hypotes 1.4 tack vare i, j, För att få resultatet, tillämpar vi återfallshypotesen till m Anmärkning: den begränsade distribuiviteten av  till över  på är avgörande i beviset för denna lemma. • Lemma 4: ).......................................................................................... Detta innebär att x i I, Av Theorem 6.1, Vi får ρ (m) = ∅. • Lemma 5: Bevis. Den del av jämställdheten är en direkt följd av det faktum att  till-anti-monotoniska för element av P(C). För den del, vi bevisar att för varje väg med minst en cykel i det, det finns en väg med en enkel cykel mindre som har en mindre summa. Låt oss bevisa att vi kan välja x 0 sådan att  skai, x 0 − x i) γ(m i0 ), och x i − x 0  till γ(m 0i ). Detta kommer att bevisa att (0, x 1 − x 0,. .., x N − x 0 )  på (m), och så ι (m) = ∅. Första anmärkningen: x i − x 0  till γ(m 0i ) Betrakta uppsättningen C = γ( 1≤i ({x i}}m i0 )). Sedan C = ∅, Anmärkning: det faktum att vi kan representera singletons, och stabiliteten i  till är avgörande i beviset för denna lemma. • Påståenden: om ρ (m) = ∅, sedan 0 = j 0 och c  ska γ(m) i0j0), finns det (x 0,. .., x N −1 )  på ett sådant sätt att x j0 − x i0 = c. Bevis. Genom upprepning på N. Fallet N = 1 är inte av intresse. När N = 2 och ρ (m) = ∅, ρ (m) = ρ (m ) = { (x 0, x 1 ) x 0 = 0, x 1 − x 0  till 01 }. Vi kan välja, utan förlust av generalitet, i 0 = 0, j 0 = 1, så c  ska γ(m) 01 ). Då är egendomen uppenbar. Antag att egenskapen är sann för vissa N > 1 och låt m vara en matris av storlek N + 1 med icke-tomma domän. Vi antar också, utan förlust av generalitet, att i 0, j 0 > 0 (N + 1 > 2, så man kan enkelt säkerställa i 0, j 0 > 0 med hjälp av en enkel variabel permutation). Vi konstruerar m′ av storlek N som i Lemma 7: i, j < N, m′ ij = m (i+1) (j+1) (m (i+1) 0  till m 0 (j+1) ). Kom ihåg att...i, j, m
a I ¥ a P, där basepa P q REF infördes svagt relationsdomäner, som är en parameteriserad familj av relationsdomäner, parameteriserade av en icke-relationell bas abstrakt domän.
A Few Graph-Based Relational Numerical Abstract Domains
{'venue': 'Static Analysis Symposium (SAS) (09/2002) 117-132', 'journal': None, 'mag_field_of_study': ['Computer Science']}