Stadgan om SRC är att främja både kunskapsläget och den senaste tekniken inom datasystem. Från vår etablering 1984 av Digital Equipment Corporation (numera Compaq) har vi bedrivit grundforskning och tillämpad forskning för att stödja företagets affärsmål. Våra intressen spänner över skalbara system (inklusive hårdvara, nätverk, distribuerade system, och programmering språk och teknik), Internet (inklusive webben, och internet apparater), och människa / dator interaktion. Vår strategi är att testa det tekniska och praktiska värdet av våra idéer genom att bygga maskin- och programvaruprototyper och använda dem som dagliga verktyg. Intressanta system är för komplexa för att utvärderas enbart i det abstrakta; utökad användning gör att vi kan undersöka deras egenskaper på djupet. Denna erfarenhet är användbar på kort sikt för att förfina vår design, och ovärderlig på lång sikt för att främja vår kunskap. De flesta av de stora framstegen i informationssystem har kommit genom denna strategi, inklusive personlig databehandling, distribuerade system och Internet. Vi utför också kompletterande arbete av en mer matematisk smak. En del av det är inom etablerade områden av teoretisk datavetenskap, såsom analys av algoritmer, beräkningsgeometri, och logik av programmering. Annat arbete utforskar ny mark som motiveras av problem som uppstår i vår systemforskning. Vi har ett starkt engagemang för att kommunicera våra resultat; att exponera och testa våra idéer i forsknings- och utvecklingsgemenskaperna leder till ökad förståelse. Vår forskningsrapportserie kompletterar publicering i professionella tidskrifter och konferenser medan vår tekniska anteckningsserie kompletterar forskningsrapporter och tidskrifts-/konferenspublikationer genom att möjliggöra snabb spridning av nya forskningsresultat. Vi söker användare för våra prototypsystem bland dem som vi har gemensamma intressen med, och vi uppmuntrar samarbete med universitetsforskare. David L. Detlefs, K. Rustan M. Leino, Greg Nelson, och James B. Saxe December 18, 1998 Författare Affiliations David L. Detlefs är en stab ingenjör på Sun Microsystems Laboratories. Han kan nås på david.detlefs@sun.com. Detta arbete slutfördes av honom och de andra författarna innan han lämnade SRC 1996. Detta verk får inte kopieras eller reproduceras helt eller delvis för något kommersiellt ändamål. Tillstånd att kopiera helt eller delvis utan betalning av avgift beviljas för ideella utbildnings- och forskningsändamål, förutsatt att alla sådana fullständiga eller partiella kopior omfattar följande: ett meddelande om att sådan kopiering sker genom tillstånd från System Research Center of Compaq Computer Corporation i Palo Alto, Kalifornien; ett erkännande av upphovsmännen och enskilda bidragsgivare till verket; och alla tillämpliga delar av meddelandet om upphovsrätt. Kopiering, återgivning eller återutgivning för något annat ändamål ska kräva licens med betalning av avgift till Systems Research Center. Alla rättigheter förbehållna. Papperet beskriver en mekanisk kontroll för programvara som fångar många vanliga programmeringsfel, i synnerhet array index begränsar fel, inga dereferensfel, och synkronisering fel i multi-trådade program. Kontrollen utförs vid kompileringstidpunkten. Kontrollen använder en automatisk teorem-provare för att resonera om semantiken av villkorliga uttalanden, loopar, procedur och metodanrop, och undantag. Kontrollen har implementerats för Modula-3. Den har tillämpats på tusentals rader av kod, inklusive mogen systemkod samt färsk oprövad kod, och den har funnit ett antal fel. Författarna till denna uppsats var fortfarande barn när de ledande ljusen i datorer förklarade att världen stod inför en "programvara kris". Medan hårdvaran förbättrades varje år, var mjukvaran fast i komplexitet, och programmeringen var dyr, felbenägen och ansträngande. Men dessa dystra observationer stoppade inte programvaruindustrin, som fortsatte att öka sina intäkter och vinster dramatiskt, och som har upprätthållit denna tillväxt med kontinuerlig innovation. Var programvarukrisen ett falskt alarm? Inte direkt. Även om lönsamma, skriva programvara är fortfarande dyrt, fel-bene, och hårda. Innovation inom programvaruindustrin har till största delen begränsats till att hitta nya saker som har att göra med programvara, och har inte hittat många nya sätt att producera programvara. Det är fortfarande vanligt att se mjukvarukatastrofer där miljontals dollar spenderas på att skriva ett program som överges innan release, eftersom implementatorerna helt enkelt inte kan få det att fungera. Det tragiska misslyckandet att etablera programvara som tillförlitlig teknisk disciplin framgår smärtsamt tydligt av studier som Leveson och Turners undersökning av Therac-25-olyckorna [31]. Även om intäkter och vinster har ökat, visar siffror från det ekonomiska konsultföretaget DRI/McGraw-Hill att produktiviteten i programvaruindustrin faktiskt har minskat under en period av allmänt ökande produktivitet under den senaste tiden [10]. Dessa beräkningar kanske inte är helt korrekta eftersom det är svårt att korrigera för inflationen, men det verkar säkert att säga att programvaruproduktiviteten inte har hållit jämna steg med produktiviteten inom andra områden inom dataindustrin såsom hårdvara. I själva verket skulle vi hävda att tillväxten av mjukvaruindustrin har trotsat stagnationen av programmeringsteknik bara på grund av den medvind som skapats av den miljonfaldiga förbättringen av pris / prestanda för processorer under de senaste trettio åren. När informationsrevolutionen lämnar sin späda barndom, och vi inom ingenjörsvärlden tar på oss ansvaret att uppfylla sina stora löften, från robotar till knowbots, anses det otillräckligt att våra framsteg skulle påskyndas enormt om programmeringstekniken avancerades på något som liknar samma kurva som mikroprocessorer. Många silverkulor har förebådats som lösningen på programvarukrisen. Om du har ett programvaruproblem är strukturerad programmering med PL/I svaret! Den objektorienterade revolutionen kommer att föra massproduktionsmetoder till programvara och göra programfragment till billiga återanvändbara pålitliga varor! Programverifiering kommer att eliminera alla fel! Programmering i naturligt språk kommer att eliminera behovet av arktiska språk; slutanvändare kommer att uttrycka sina krav direkt till datorn, och programmering som ett yrke kommer att vissna bort! Ingen av drömmarna bakom dessa slagord har uppfyllts. Vi anser att programplaneringen och dess svårigheter är här för att stanna. race villkor i multi-trådade program. Verktyget är användbart eftersom kostnaden för ett fel minskar kraftigt om det upptäcks tidigt i utvecklingsprocessen. Verktyget är avsett att vara som en typkontroll eller som C-verktyget lint [23]: dess varningar är avsedda att tolkas av programförfattaren som kontrolleras. Kontrollen genomförs med hjälp av tekniken för programverifiering. Programmet kommenteras med specifikationer; det kommenterade programmet presenteras för en "verifiering villkor generator", som producerar logiska formler som är bevisbara om och endast om programmet är fri från den särskilda klassen av fel som övervägs, och dessa formler presenteras för en automatisk teorem-prover. Detta låter som programverifiering, men det är inte: för det första eftersom vi inte försöker bevisa att ett program gör vad det är tänkt att göra, bara för att kontrollera vissa specifika typer av fel; för det andra eftersom vi är intresserade av misslyckade bevis bara, inte i framgångsrika. En avgörande punkt är att misslyckade bevis är mer användbara än framgångsrika, eftersom de varnar programmeraren för eventuella fel. Förutom att vara mer användbar är ESC mer genomförbart än fullskalig programverifiering. Till exempel är en osund fullskalig programkontrollant en oxymoron, men mängden osundhet att tolerera i en statisk kontroll är en fråga om teknisk bedömning: ingen förväntar sig en typkontroll eller ett lint verktyg för att hitta alla fel; dess verktyg bestäms av antalet fel den hittar vägs mot kostnaden för att köra verktyget. På samma sätt, eftersom vi inte lovar att ESK kommer att upptäcka alla fel, är vi fria att förklara att vissa typer av fel ligger utanför verktygets räckvidd. Denna idé om utökad statisk kontroll är inte ny. Den första doktorsavhandlingen som vi känner till tog upp idén var av Dick Sites för ett kvarts sekel sedan [44], och problemet har hållit sig som ett avhandlingsämne ända sedan dess. Men de forskningsprototypkontroller som har genomförts under årtiondena har gjort alltför många förenklade antaganden. De får inte hantera dynamiskt fördelade data eller objektorienterad programmering; de får inte hantera konvergens; de kan kräva källan för hela programmet för att kontrollera någon del av det; de kan kräva att användaren vägleder teoremet-provaren eller för att ge komplicerade loopinvarianter. Sådana förenklingsantaganden är ett sätt att skilja oron åt, vilket kan bidra till att fokusera på särskilda aspekter av problemet och på så sätt fördjupa insikten. Vårt arbete bygger på de djupa insikter som många tidigare forskare har skapat, men vårt ESC-projekt har följt ett kompletterande forskningssätt, där varje två ansträngning görs för att producera och testa en realistisk artefakt. Detta kompletterande forskningssätt kan ofta avslöja överraskningar. De flesta tidigare kontrollverktyg testades endast på små program skrivna av verktygsimplementatorerna själva. Däremot var vår plan att köra vår checker på betydande delar av Modula-3 runtime-systemet. Genom att ta itu med realistiska program som skrivits av andra (eller i vissa fall av ESK:s projektmedlemmar innan ESK-projektet inleddes) hoppades vi få svar på följande frågor: • Kan vi skapa kontrollvillkor för sådana "systemprogram"? • Skulle vi kunna omvandla misslyckade verifieringar till specifika felmeddelanden? • Hur stor börda skulle det vara att skriva de nödvändiga kommentarerna? • I vilken utsträckning kan vi automatisera den teorem-proving uppgiften? Sammanfattningsvis var vi fast beslutna att stresstesta en idé som länge varit i havandeskap. Vår kontroll hanterar multi-trådade multi-modul objektorienterade program. Vår kontroll fungerar på Modula-3 program [40], men teknikerna skulle fungera för alla språk på vilka adressen aritmetisk är begränsad, inklusive Java, Ada, Oberon, och FORTRAN. När detta dokument går till tryck, har ett uppföljningsprojekt kopierat tekniken i ett verktyg för Java. Vår kontroll utför modulär kontroll: du kan använda den för att kontrollera valda moduler i ett program utan att kontrollera hela programmet. Eftersom modern programmering är otänkbar utan bibliotek, anser vi att modulär kontroll är nödvändig. Kontrollen gör det också möjligt för dig att kontrollera valda klasser av fel; till exempel är det ofta användbart att kontrollera dödläge och tävlingsförhållanden utan att kontrollera för array indexgränser fel. När kontrollören ger falska varningar finns det en mängd olika sätt att undertrycka dem, det vill säga att få kontrollanten att ignorera de falska varningarna och fortsätta att rapportera verkliga fel. A Även om vår kontroll är en forskningsprototyp, med många grova kanter, anser vi att den visar löftet om tekniken tydligare än tidigare kontroller: ESC fångar fel som ingen typkontroll kan fånga, men det känns för programmeraren mer som en typkontrollör än en programkontrollant. De specifikationer som krävs är uttalanden av enkla fakta som ojämlikheter, felmeddelandena är specifika och korrekta med avseende på källposition och feltyp, och teorem-proving utförs bakom kulisserna automatiskt. Vårt huvudsakliga mål för detta papper är att förmedla till läsaren hur det känns att använda en kontroll som fungerar i denna mellanliggande nivå mellan typkontroll och verifiering. Dokumentet består därför till stor del av två exempel. Efter exemplen beskriver vi på en ganska allmän nivå några av de nya aspekterna av vår kontroll, men vi har förvisat många detaljer till andra papper. I detta avsnitt lägger vi grunden till de exempel som utgör kärnan i dokumentet genom att kortfattat presentera ESK:s språkspecifikation. Utformningen av specifikationsspråket återspeglar strukturen av väl utformade program. En pelare i programstrukturen är procedurmässig abstraktion, där en sammansatt operation namnges och parameteriseras och används av resten av programmet som om det vore en elementär operation. Procedural abstraktion gör statisk analys svår, så svår att många statiska analysmetoder som beskrivs i litteraturen endast gäller program utan procedurer, och många praktiska kompilatorer utför ingen interprocedural analys alls, även om de utför omfattande intra-procedural analys. Anledningen till detta är att upphovsmännen till kompilatorer och andra verktyg inte har velat förlita sig på specifikationer, men inter-förfarandeanalys kräver i grunden att man behandlar specifikationer, oavsett om de tillhandahålls av programmeraren eller kan härledas från verktyget. För att utföra en interprocessell analys använder sig ESC av specifikationer för programmerare som tillhandahålls av det formulär som visas i figur 0. För- och postvillkor är formler i en första-order teori som inkluderar Modula-3 inbyggda operatörer. En förfarandespecifikation är ett avtal mellan exploatören och kunden: klienten avtal att kalla förfarandet i ett tillstånd där förutsättningarna är sanna, och exploatören avtal (a) att ändra ingen variabel utom de i MODI-FIES-listan, och (b) att återvända endast i ett tillstånd som uppfyller postvillkoret. Vid kontrollen av förfarandets helhet utgår ESK från att förutsättningarna är uppfyllda från början och kontrollerar att när förfarandet återställs är villkoren uppfyllda och att endast dessa variabler i MODIFIES-klausulen har ändrats. Omvänt kontrollerar ESK vid kontroll av en kund att villkoret är uppfyllt vid ansökningsomgången och utgår från att ansökningsomgången respekterar både postvillkoret och MODIFIES-klausulen. Här finns till exempel en Modula-3-deklaration och ESC-specifikation för en enkel slumptalsgenerator: MODIFIES utsäde REQUES 0 < n OCH utsäde # 0 ENSURES 0 RES OCH RES < n OCH utsäde # 0 * > Exemplet illustrerar också flera andra punkter. För det första, för en variabel som förtecknas i MODIFIES-klausulen (t.ex. utsäde), kan förekomster i postvillkoret vara oprimerade eller primerade (frö). En primerad händelse betecknar värdet av variabeln i post-tillståndet, medan en oprimerad händelse betecknar värdet av variabeln i för-tillståndet. För det andra används det reserverade namnet förnybara energikällor för att ange resultatet av förfarandet, i förekommande fall. För det tredje omger Modula-3 pragma-fästen, <* *>, ESK-anteckningar för att skilja dem från vanliga Modula-3. Fjärde, x # y är Modula-3 syntax för att hävda att värdena för x och y är olika. En annan pelare i programstrukturen är dataabstraction, där en samling av programvariabler (eller konkreta variabler) anses begreppsmässigt representera en enda abstrakt variabel. Den abstrakta variabeln används av klienter för att resonera om verksamhetens semantiska effekt på abstraktionen, och de konkreta variablerna används av implementeringen för att fungera effektivt på staten. Till exempel, det abstrakta värdet av ett komplext tal z kunde representeras konkret i termer av två flyttal Cartesian koordinater z.x och z.y; alternativt samma abstraktion kan representeras i termer av polar koordinaterna z.r och z.theta. I allmänhet är modulstrukturen i ett program arrangerad så att den konkreta representationen av en abstraktion är osynlig (dvs utom räckhåll) inom de moduler som använder abstraktionen (dess kunder) [42]. Figur 1 visar ESK:s syntax för att förklara en abstrakt variabel och ange dess representation (även känd som dess abstraktionsfunktion). Till exempel, 5 < * SPEC VAR a: INTEGER *> VAR c: INTEGER; < * SPEC REP a = c * c * > förklarar ett abstrakt heltal variabel a, ett konkret heltal variabel c, och anger att kvadraten c representerar a. Vi har inte beskrivit hela specifikationsspråket, men vi har beskrivit tillräckligt för att ge det första exemplet. Båda de två utökade exemplen i detta papper använder Modula-3's standard I/O-bibliotek, som är utformat kring den viktiga abstraktionen av en övervakad objektorienterad buffrad ström. I synnerhet är en läsare en ingångsström och en författare är en utgångsström. Varje stream objekt innehåller en buffert och metoder för att hantera bufferten. Olika strömunderklasser åsidosätter metoderna på olika sätt, så att till exempel en filläsare fyller på bufferten från disken och en nätverksläsare fyller på bufferten från nätverket. Klassoberoende kod kan vara gemensam för alla underklasser; till exempel, Wr.PutInt skriver ASCII representation av ett heltal i en författares buffert. Modula-3 design beskrivs i kapitel 6 i Nelsons Modula-3 bok [40], den ursprungliga designen beskrivs av Stoy och Strachey [46]. Vi beskriver olika aspekter av de relevanta gränssnitten eftersom vi behöver dem för våra exempel. För varje typ av ström tillhandahåller Modula-3 I/O-biblioteket två gränssnitt, ett grundläggande gränssnitt för enkla kunder och ett avancerat gränssnitt som erbjuder ytterligare funktionalitet (särskilt tillgång till buffertstrukturen) till priset av ytterligare komplexitet. Det grundläggande skribentgränssnittet. Vårt första exempel använder bara det grundläggande skrivgränssnittet Wr, som presenteras i figur 2. Här är en översättning av figur 2 från Modula-3 till engelska. Författaren klass ges det globala namnet Wr.T, där Wr är namnet på gränssnittet och T är enligt överenskommelse den huvudsakliga typen som anges i gränssnittet. Klassen deklareras som en ogenomskinlig objekttyp, allmänt känd endast som en subtyp av den inbyggda klassen ROOT. (I Modula-3 motsvarar klasser objekttyper.) Den faktiska deklarationen av representationstyp är dold i det avancerade gränssnittet, och är osynlig för kunder i det grundläggande gränssnittet. Förfarandena PutChar, PutText och Stäng har givna signaturer och specifikationer (TEXT är Modula-3:s fördeklarerade strängtyp)..) Ett U-värdesatt fält f som deklareras i en klass T motsvarar semantiskt en karta från T till U. Således kan de giltiga och statliga deklarationerna betraktas som BOOLEAN-värderade och ANY-värderade fält av författare. Även Modula-3 använder syntax x.f för att beteckna f-fältet i ett objekt x, annotationsspråket använder syntax f[x] när f är abstrakt. Specifikationerna för skrivgränssnittet faller in i ett gemensamt mönster som vi kallar tillstånd/validitetsparadigm. I detta paradigm finns det två abstrakta variabler, giltiga och tillstånd. Tanken är att giltig [wr] representerar villkoret att wr är en korrekt initierad giltig författare, och stat[wr] representerar alla andra tillstånd av wr (till exempel dess innehåll och position). Om vi gjorde fullskalig programverifiering, det skulle finnas sidor av specifikationer om tillstånd, men eftersom vi gör utökad statisk kontroll bara, det finns nästan ingenting att säga om tillstånd, förutom att specificera att vissa förfaranden kan ändra det. (Inte ens typen av tillstånd är relevant, så vi använder den speciella ESC-typen NÅGON.) I tillstånd/validitetsparadigmet blir specifikationerna mycket stiliserade. En typisk procedur eller metod som fungerar på en författare wr (som PutChar) har specifikationen Eftersom giltig inte visas i MODIFIES-listan, innebär denna specifikation att giltigheten bevaras. Ofta några förfaranden kommer att ha några ytterligare kommentarer-till exempel PutText kräver att dess text argument är icke-NIL-men för enkla gränssnitt stiliserade specifikationer av tillstånd/validitet paradigm är lejonparten av vad som måste skrivas för en ESC-verifikation. Textförfattarens gränssnitt. Figur 3 illustrerar textförfattarens gränssnitt, en viss skrivarunderklass som förekommer i vårt exempel. En textförfattare är en författare som inte gör någon utmatning; den lagrar bara allt som har skrivits i en intern buffert och tillhandahåller en procedur GetText som returnerar innehållet i bufferten som en TEXT. Eftersom TextWr.T är en underklass av Wr.T, specifikationsvariabler giltiga och tillstånd gäller för textförfattare, och används i specifikationen av textförfattare gränssnittet. Metoden init initierar en textförfattare (etablerar giltig"[twt]) och returnerar den (etablerar RES=twt). Specifikationen är helt typisk för initieringsmetoder i tillstånd/validitetsparadigmet. Likaså, specifikationen av GetText är typisk för tillstånd/giltighet paradigm, med ytterligare en postvillkor conjunkct RES # NIL. Exempel. Vårt första exempelprogram är den typ av elementär programmeringsövning som kan tilldelas elever som först lär sig att programmera med utgångsströmmar, och vi har sått vårt program med elementära fel. Problemet är att programmera en procedur som tar en rad texter som argument och returnerar en enda text som innehåller konkatetering av alla texter i arrayen. Detta kan göras ganska enkelt genom att upprepade gånger kalla Modula-3 binär konkatetering operation Text.Kat, men att göra så leder till en prestanda fälla, eftersom med de flesta implementationer av text concatenation, den totala kostnaden i tid för denna enkla strategi kan vara proportionell mot kvadraten på längden på det slutliga resultatet. Ett bra sätt att undvika denna quadratic kostnad är att använda en text författare, vilket leder oss till förfarandet ArrayCat visas i Figur 4. Förfarandet allokerar en textförfattare, skriver elementen i arrayen till skribenten i ordning, och slutligen hämtar och returnerar en text som innehåller allt som skrivits. (Detta tillvägagångssätt undviker den kvadratiska kostnaden om textförfattare är väl genomförda.) Köra ESC på ArrayCat proceduren i Figur 4 ger en varning om en matris indexgränser fel: array index gränser fel, rad 4: (Det exakta formatet för ett ESC felmeddelande är identiskt med ett kompilator felmeddelande; i detta papper använder vi kursiv stil och understrykning för att förmedla samma information.) Felmeddelandet innehåller också en så kallad "terror kontext" som är en lång lista över atomformler som kännetecknar den situation där felet kan inträffa. Eftersom det är långt, kommer vi inte att visa fel sammanhang här, men vi noterar att en studie av sammanhanget avslöjar att det innebär formeln i=NUMBER(a), vilket i själva verket är det tillstånd i vilket matrisen gränser fel kan inträffa: i Modula-3, öppna matriser indexeras från 0, men FOR slingan skrevs som om de var indexerade från 1. Att korrigera felet på ett naturligt sätt ger följande En studie av felsammanhanget visar att det innebär formeln INTE giltig [twr]. Det vill säga, ESC har upptäckt och varnat för misslyckandet med att initiera twr (programmet tilldelade textförfattaren, men misslyckades med att initiera den). För att rätta till detta fel lägger vi till en uppmaning till initmetoden, som kräver att man infogar de sju tecknen ".init()": Denna korrigering eliminerar båda de tidigare varningarna, men ESC ger ytterligare en varning: förutsättningen misslyckades, rad 4: En studie av felsammanhanget visar att TEXT-argumentet till PutText är lika med NIL, vilket är förbjudet av förutsättningen för PutText men inte säkerställt av ArrayCat, som blint passerar a[i], oavsett om det är NIL eller inte. Detta fel tvingar en omprövning av utformningen för ArrayCat: vad ska vi göra om NIL poster i TEXT array? Två konstruktioner kommer genast att tänka på: att ignorera NILs eller att förbjuda NILs. Antingen design är lätt att ta sig igenom ESC. I den design där NILs ignoreras omkodas förfarandet enligt följande: och naturligtvis ESC, som förstår IF uttalanden, är helt nöjd med denna version. I den konstruktion där NIL är förbjudet förstärks specifikationen för ArrayCat med en kvantifierad förutsättning: ESC är också helt nöjd med denna design: den starkare förutsättningen undertrycker felmeddelandet. Dessutom kommer ESK att upprätthålla den starkare förutsättningen var ArrayCat än kallas. Vi vill göra flera kommentarer om detta exempel. För det första, även om det krävdes noggranna specifikationer för skribentens och textförfattarens gränssnitt, kunde den inledande programmeraren använda sig av ESC utan att alls skriva några specifikationer för sitt program. Inga förutsättningar eller loopinvarianter krävdes i ArrayCat. Vi anser att detta är som det bör vara: alla som är kvalificerade att utforma gränssnitten i ett strömmande bibliotek förstår förutsättningar och postvillkor och abstraktioner på någon nivå, och kommer att finna att en uttrycklig notation för deras designbeslut är ett användbart verktyg snarare än en börda. Å andra sidan kan och bör många enkla fel i program identifieras genom att läsa det oannoterade felaktiga programmet; att kräva en loop invariant för att kontrollera ArrayCat verkar pedagogisk och tunghänt. För det andra bör läsaren vara medveten om att vi, även om vi i detta exempel har koncentrerat oss på att kontrollera en klient till I/O-systemet, faktiskt också har använt ESK för att kontrollera genomförandet av textförfattare. Vid genomförandet görs en representationsförklaring för att ge den konkreta innebörden av giltig [twr] när det gäller de konkreta fälten för twr. Och denna representation används av ESC när man kontrollerar de förfaranden som PutText och GetText, som kräver giltighet som en förutsättning och vars genomförande beror på den konkreta betydelsen av giltighet. En tredje anmärkning som detta exempel tillåter oss att göra är att det är upp till användaren att välja en punkt på kontinuum mellan fullständig funktionskorrigering 12 och minimal utökad statisk kontroll. Det är till exempel sant att det är tomt att initiera en textskribent, men våra specifikationer återspeglade inte denna sanning. Om vi ville skulle vi kunna återspegla detta genom att stärka villkoren för init i följande riktningar:. Dessutom är notationen "" faktiskt inte korrekt för den tomma teckensekvensen.) Det skulle vara lätt att skapa ett konstgjort exempel där denna starkare specifikation skulle vara nödvändig för en viss ESC-kontroll. Till exempel, avsaknaden av array gränser fel i vissa klient kan bero på det faktum att en ny initierad text författare är tom. Men det här är en hal sluttning. Om dess effekt på staten är helt specificerad, varför inte PutChar's också? Utan disciplin kan du snabbt glida in i det svarta hålet med fullständig korrekthetsverifiering. Lyckligtvis har vår erfarenhet varit att många ESC-verifikationer med framgång kan slutföras med nästan inga specifikationer alls om innehåll och betydelser av abstrakta typer, förutom specifikationen av giltighet. Du kan gå en lång väg bara förlita sig på tillstånd / giltighet paradigm: det vill säga specifikationerna för varje förfarande registrera exakt hur förfarandet påverkar och kräver giltighet, men alla andra biverkningar sopas under den rikliga mattan av MODIFIES tillstånd [wr]. Vi anser att detta är ett viktigt skäl till att ESK:s kontroller kan vara mer kostnadseffektiva än fullständiga korrekthetskontroller. I detta avsnitt kommer vi att beskriva användningen av ESC på ett mer sofistikerat program, WhiteSpace. Läs mer. Exemplet är också ett kort klientprogram för Modula-3 I/O-systemet, men skiljer sig på flera sätt från exemplet i föregående avsnitt. En ganska liten skillnad är att detta program är en klient av inflöden snarare än utflöden. En viktigare skillnad är att vi i detta exempel kommer att uppmärksamma synkroniseringsprotokollet som är utformat för både läsare och författare. I det föregående exemplet utelämnade vi synkroniseringen för att förenkla utställningen. En annan viktig skillnad är att i detta avsnitt kommer vi att se ett program som använder det avancerade gränssnittet för att hantera buffertstrukturen i strömmen, istället för att uteslutande använda procedurerna i det grundläggande gränssnittet. PROTECT v BY mu delad variabel v är inte att komma åt utan att hålla låset mu PROTECT f BY SELF för varje objekt t, delade fält t.f inte ska nås utan att hålla låset t LL uppsättning lås som hålls av den aktuella tråden supremum (maximum) i programmeraren deklarerad låsordning Figur 5: Låsnivå syntax. Den andra formen av PROTECT kan endast användas när f är ett fält som deklareras i en underklass av MUTEX. Hur ESC kontrollerar synkroniseringsfel. Vår erfarenhet har varit att många synkroniseringsfel är misslyckanden att förvärva lås (orsakar rasförhållanden) eller förvärva lås ur ordning (orsakar dödläge). Därför har vi utformat ESK-anmärkningsspråket för att fånga upp dessa enkla fel; figur 5 visar syntaxen. Programmeraren förklarar vilka lås som skyddar vilka delade variabler och vilka lås som kan eller måste hållas vid inträde i olika förfaranden. Programmeraren deklarerar också en partiell ordning i vilken trådar tillåts förvärva lås. ESC kontrollerar att delade variabler aldrig nås utan att hålla låset som skyddar dem, och även kontrollerar att trådar förvärvar lås i strikt ökande ordning (Modula-3 har icke-mottagare lås). Detta bevisar inte korrekthet-dyrare tekniker som övervaka invarianter skulle krävas för det-men det fångar många vanliga fel. Låsordningen på mutexes betecknas med " <", och programmeraren anger den med hjälp av en allmän anordning för att lägga axioms till en ESC-verifiering: SPEC AXIOM. Till exempel, Modula-3 fönster systemet är baserat på ett objekt som kallas en VBT. VBTs arrangeras i träd, och kan låsas endast från ett blad av trädet mot roten, inte vice versa. Denna regel deklareras i VBT-gränssnittet enligt följande: Axioms om låsordningen uppstår endast i subtila situationer. I synnerhet, exemplet vi är på väg att presentera förvärvar endast en läsare lås i taget, så vi behöver inte deklarera axioms om låsordningen. Det grundläggande läsgränssnittet. Figur 6 visar det grundläggande Modula-3-gränssnittet Rd, inklusive dess ESC-specifikationer. De enda nya inslagen i figur 6 avser samstämmighet. Synkroniseringsprotokollet för läsarna är mycket stiliserat, vi kallar det för det övervakade objektparadigmet: Ett objekt behandlas som en övervakare i det att ömsesidig uteslutning tillhandahålls för trådar som fungerar på objektet via procedur 15 samtal och metodsamtal. Den ömsesidiga uteslutningen uppnås genom att själva objektet låses, vars typ är en subtyp av MUTEX, Modula-3s predeklarerade ömsesidiga uteslutningstyp. Att förvärva låset är detsamma som att gå in i monitorn. Texten i gränssnittet i figur 6 återspeglar det övervakade objektparadigmet på två sätt. För det första förklaras Rd.T vara en ogenomskinlig subtyp inte av ROOT utan av MU-TEX. För det andra har kontrollförfarandena det extra förhandsvillkoret supp(LL) < rd, vilket återspeglar kravet att de ska kallas från ett land där det är lagligt att förvärva låset rd. Det avancerade läsgränssnittet. Det grundläggande Rd-gränssnittet är det som används av de flesta enkla klienter, men det är otillräckligt för mer sofistikerade kunder. Till exempel, eftersom det döljer bufferten och metoden för påfyllning av bufferten, är det otillräckligt för kunder som implementerar nya klasser av läsare. Figur 7 visar RdrRep-gränssnittet, som ger de specifikationer som behövs för mer sofistikerade kunder. Med RdrRep gränssnittet kommer vi bortom pannplatta ESC specifikation paradigm, och börja sätta specifikationsspråket genom sina steg. Gränssnittet börjar med att avslöja representationen av typen Rd.T, som är ogenomskinlig i det grundläggande gränssnittet. Representationen är en objekttyp som innehåller ett buff-fält, vilket är en hänvisning till en rad tecken. Modula-3-nyckelordet BRANDED ersätter namnet ekvivalens för Modula-3:s standardstrukturell ekvivalens för typer. Förutom buff fältet, Rd.T innehåller också flera heltal och booleska fält. heltalsfälten bestämma den aktiva delen av bufferten, enligt en konvention illustrerad i figur 8. De booleska fälten är irrelevanta för detta exempel. Det fullständiga gränssnittet innehåller flera metoder, men vi visar bara sökmetoden, eftersom de andra är irrelevanta för vårt exempel. SPEC PROTECT-anteckningen anger att en läsares fält skyddas av läsaren själv, dvs. en tråd får inte läsa eller skriva något av läsarens fält om den inte har förvärvat läslåset. Denna kommentar är typisk för det övervakade objektparadigmet. Därefter kommer vi till specifikationen av sökandet. Denna metod är ansvarig för att utföra den klassspecifika beräkning som ingår i omplaceringen av bufferten: anropet rd.seek(n) ändrar bufferten så att byte nummer n av läsarens källa finns i bufferten. I synnerhet rd.seek (rd.hi) kommer att gå vidare till nästa buffert av data (eftersom rd.hi är indexet för den första byte som är bortom den nuvarande bufferten av data). Metoden returnerar SeekResult.Ready om omplaceringen är framgångsrik; om n är bortom slutet av läsaren, den returnerar SeekResult.Eof. (Om DontBlock är inställd och sökmetoden inte kan göra sitt jobb utan att riskera blockering, är det tillåtet att returnera SeekResult.
Ett intressant exempel på ett sådant verktyg är ESC/Java Ref.
Extended static checking
{'venue': 'PROCOMET', 'journal': None, 'mag_field_of_study': ['Computer Science']}