En teori, grafisk notation, matematisk analys och implementation för att hitta om två givna uttryck kan, vid exekveringstidpunkten, beteckna referenser knutna till samma objekt. Avsedd som utsäde för en heltäckande lösning på "frame problem" och som ett alternativ (för den specifika frågan om att bestämma alias) till separation logik, form analys, ägandetyper och dynamiska ramar 1. Du har säkert läst Homer. Jag har inte (för mycket blod), men då lyssnar jag mycket på Offenbach, så vi delar lite kunskap: vi förstår båda att "den vackra dottern Leda och svanen", "fattiga Menelaus make" och "Pâris älskare" alla betecknar samma person, även känd som Helen av Troja. De många sätten att kalla Helen är ett fall av alias, människans förmåga att beteckna ett enda objekt med mer än ett namn. Aliasing är på sin högsta risk att orsaka förvirring när det är dynamiskt, det vill säga när ett objekt kan när som helst få ett nytt namn, särskilt om det namnet tidigare betecknat ett annat objekt. Uttrycket " Jag tyckte att Pâris älskare var dåligt klädd " ger inte nödvändigtvis upphov åt agg mot Helens sartoriala smaker, som Pâris vid det här laget kanske har funnit sig vara en ny älskare; men om vi inte noggrant följer de rikas och berömdas liv kanske vi tror att det gör det. Berättelser om ödesdigra konsekvenser av dynamiskt alias överflöd av liv, litteratur och drama. Det finns även en opera, Smetana's Brud Såld 2, vars tomt helt vilar på en enda alias händelse. Till bybornas bestörtning lovar Jeník äktenskapsmäklaren, i utbyte mot goda pengar, att inte avråda sin älskling Mařenka från att gifta sig med bondens son Mícha. I själva verket vill Mícha Mařenka för sin dumbom son, Vašek, men det avslöjas plötsligt att Jeník, som fram till dess troddes vara en främling i byn, är Míchas son från ett första äktenskap: han har lurat alla. För en programmerare låter denna berättelse bekant: motsvarigheten i programutförande är att utföra en operation på vissa operander, och oavsiktligt att ändra en egenskap hos ett mål som inte nämns i operationen - därav risken för förvirring - men aliased till en av operanderna. Till exempel kan en operation officiellt ändra värdet av x.a; men om x betecknar en referens och y en annan referens som sker vid tidpunkten för utförandet som alias till x (vilket innebär att de båda pekar på samma objekt), operationen kommer att ha en effekt på y.a även om dess text inte nämner y. Om b är aliased till a, kan vi även ha en operation som ändrar y.b även om dess beskrivning i programmeringsspråket varken nämner y eller b. _______________________ Det är inte svårt att motivera det fortsatta sökandet efter effektiva verifieringsmetoder som omfattar alias. I det nuvarande tillstånd av bevisteknik, är alias problemet (tillsammans med nära relaterade ram problem, som det ger nyckeln) det främsta hindret för fullständiga bevis på korrekthet för sekventiella program. Det spelar också en roll i de specifika svårigheterna att bevisa samtidiga program korrekt. (För referenser om de frågor och tillvägagångssätt som nämns i detta avsnitt, se bilaga F.) Ett symptom på denna situation är att industriella program som bevisar verktyg ofta utesluter användning av pekare helt och hållet. Ett exempel är Spark-miljön, som har bidragit på ett anmärkningsvärt sätt till att visa att produktionsprogram rutinmässigt kan utsättas för beviskrav. Spark bygger på ett programmeringsspråk, som presenteras som en delmängd av Ada men i verkligheten en delmängd av ett Pascal-liknande språk (plus moduler), utan stöd för pekare eller referenser. När man överväger hur man skall göra sådana banbrytande framsteg relevanta för en större del av branschen, är det svårt att föreställa sig att massor av programmerare avstår från pekare och andra programmeringsspråk framsteg under de senaste tre decennierna. Avsaknaden av en allmänt accepterad lösning beror inte på bristande försök. Problemet med alias har undersökts ingående och intressanta lösningar har föreslagits, särskilt formanalys, separationslogik, ägartyper och dynamiska ramar. Få allmänt använda bevismiljöer har integrerat dessa tekniker. Det kan fortfarande hända, men hindren är betydande. Framför allt lider de två första tillvägagångssätten (enligt vår mening) av att försöka ta en bild av den run-time pekarstruktur som är mer exakt än vad som behövs för alias analys; och de tre sista förutsätter en kompletterande notation ansträngning (utöver standard Hoare påståenden) som programmerare kan dra tillbaka. Den teori, kalkyl och prototypimplementering som beskrivs här strävar efter att undvika dessa begränsningar. En representativ ansökan är att bevisa avsaknaden av alias mellan element i två länkade listor som skapats och modifierats genom typiska objektorienterade tekniker. Anta ett standardgenomförande av förteckningar med en insats för att lägga till element i slutet:
Men separation logik och form analys försöker avslöja en mer detaljerad struktur av pekare än det är nödvändigt för alias analys Ref.
Steps towards a theory and calculus of aliasing
{'venue': 'International Journal of Software and Informaticsspecial issue (Festschrift in honor of Manfred Broy), Chinese Academy of Sciences, 2011, pages 77-116', 'journal': None, 'mag_field_of_study': ['Computer Science']}