Hur definieras funktioner och semantik på syntaktiska domäner genom strukturell induktion?

Strukturell induktion är en kraftfull metod både för att bevisa egenskaper om syntaktiska domäner och för att definiera funktioner på dessa domäner. När man tillämpar induktion på syntaktiska domäner, antas att alla fraser som konstrueras vid ett givet steg redan har en viss egenskap, och målet är att visa att de nya fraser som byggs i nästa steg bevarar denna egenskap. Genom att börja från den tomma mängden av fraser kan man säkerställa att alla fraser som genereras har denna egenskap, eftersom alla fraser i domänen definieras av dessa konstruktioner. Detta innebär att varje phrase inom domänen kommer att uppfylla den definierade egenskapen.

Förutom att användas som bevismetod kan strukturell induktion även tillämpas för att definiera funktioner på syntaktiska domäner. När man definierar sådana funktioner markerar man vanligtvis syntaktiska fraser med dubbla hakparenteser [ · ] för att tydligt separera dessa från den omgivande kontexten. Förutom variabler representeras alla symboler inom hakparenteserna som terminaler i den underliggande grammatiken. Ett exempel på detta är funktionen mult, som räknar antalet förekomster av symbolen × i ett uttryck:

• mult: Expression → ℕ

• mult[ N ] ≔ 0

• mult[ E1 + E2 ] ≔ mult[ E1 ] + mult[ E2 ]

• mult[ E1 × E2 ] ≔ 1 + mult[ E1 ] + mult[ E2 ]

Med denna definition kan man t.ex. räkna förekomster av × i uttrycket (N1 × N2) + N3 och finna att det finns exakt en förekomst.

När dessa ekvationer definierar en funktion, ersätts funktionens tillämpning som matchar den vänstra sidan av ekvationen med ett term som bestäms av den högra sidan. Eftersom varje fras i domänen endast har ett begränsat antal underfraser, kommer denna ersättningsprocess att upprepas ett ändligt antal gånger innan ingen ytterligare funktionstillämpning är möjlig.

Vid användning av strukturell induktion för att bevisa egenskaper om funktioner som definieras på syntaktiska domäner, säkerställer denna process att funktioner beskrivs på ett entydigt sätt. Ett exempel på detta är funktionen swap, som byter ordningen på argumenten för addition (+) i ett uttryck. Genom att använda strukturell induktion kan man bevisa att mult(swap[E]) = mult[E] för alla uttryck E.

Exempelvis kan semantiken för uttrycken på en viss sida definieras med en värderingsfunktion som mappar uttryck och tal till naturliga tal. Värderingsfunktionen kan se ut på följande sätt:

• [ · ] : Expression → ℕ

• [ N ] ≔ [ N ]

• [ E1 + E2 ] ≔ [ E1 ] + [ E2 ]

• [ E1 × E2 ] ≔ [ E1 ] · [ E2 ]

På detta sätt definieras semantiken för aritmetiska uttryck där naturliga tal representeras av tal och operationer som addition och multiplikation utförs på dessa tal. För att illustrera detta kan uttrycket 10 × (11 + 1) värderas till:

• [ 10 × (11 + 1) ] = [ 10 ] · [ 11 + 1 ] = [ 10 ] · ([ 11 ] + [ 1 ]) = (2 · [ 1 ]) · (2 · [ 1 ] + 1) + [ 1 ] = 2 · 4 = 8

Denotational semantik har en viktig egenskap: kompositionalitet. Detta innebär att denotationer för sammansatta fraser kan beräknas utifrån denotationerna för deras underfraser. Detta gör förståelsen av uttryck och argumentation om dem mycket enklare.

Det är viktigt att förstå att semantiken inte alltid behöver vara begränsad till naturliga tal. I mer komplexa fall kan denotationen vara en funktion på naturliga tal, där symboler i grammatikens regler representerar funktioner istället för värden. Detta gör det möjligt att hantera uttryck där vissa symboler representerar funktionella beroenden, som i fallet med funktionella program.

Endtext

Hur man verifierar systemets invarians i samtidiga system

För att förstå och verifiera invarians i samtidiga system måste vi först definiera de relevanta tillstånd och transitionssystem som beskriver programmets beteende. Låt oss ta ett exempel med två trådar som delar på resurser, där varje tråd har en cyklisk sekvens av åtgärder som den utför, kallade kritiska regioner. Detta är ett vanligt scenario i samtidiga system där vi vill säkerställa att de inte överlappar varandra i sina kritiska sektioner, vilket kan leda till felaktiga resultat eller deadlocks.

I vårt exempel definieras ett delat system med en semafor, som styr när en tråd får gå in i sin kritiska region. Semaforens tillstånd representeras av en variabel s, som kan ha värdena 0 eller 1, där 1 innebär att resursen är tillgänglig. Varje tråd har också sin egen tillståndsvariabel a respektive b, som fungerar som en programräknare för att hålla reda på vilket steg tråden är i. När en tråd går in i sin kritiska region, ändras semaforens värde, och den andra tråden måste vänta tills resursen släpps.

Varje åtgärd i systemet är beroende av att vissa villkor är uppfyllda innan den kan genomföras. Till exempel, om tråden A ska låsa semaforen för att gå in i sin kritiska region, måste semaforen vara i tillståndet 1 och a vara 0, vilket indikerar att tråden A inte är i den kritiska regionen. När semaforen låses, ändras dess värde till 0 och programräknaren för tråden A sätts till 1. När tråden A slutför sitt arbete i den kritiska regionen, släpps semaforen och trådens programräknare sätts tillbaka till 0.

För att verifiera systemets invarians – det vill säga att ingen av trådarna går in i sina kritiska regioner samtidigt – måste vi definiera en formel som beskriver detta villkor. Detta görs genom att formulera ett predikat som säkerställer att om tråd A är i sin kritiska region, så är tråd B inte i sin kritiska region, och vice versa.

Ett viktigt inslag i denna verifiering är att vi måste definiera ett starkare invariansvillkor än bara att trådarna inte kan vara i samma tillstånd samtidigt, eftersom det inte är tillräckligt för att bevisa att inga fel uppstår. Det handlar om att formulera en mer detaljerad invariant som noggrant beskriver alla möjliga tillstånd och övergångar i systemet, vilket gör det möjligt att garantera att ingen tråd kommer att gå in i sin kritiska region samtidigt som en annan tråd redan är där.

För att formellt uttrycka detta, definierar vi en systeminvariant som säger att om en tråd är i den kritiska regionen, så är den semafor som styr tillgången till resursen låst (dvs. s = 0) och den andra tråden kan inte vara i sin kritiska region. Detta garanterar att bara en tråd får tillgång till resursen åt gången.

När vi analyserar systemet måste vi också ta hänsyn till andra viktiga aspekter som kan påverka verifikationen. Till exempel, om systemet är komplext och har flera trådar som kan interagera med varandra på olika sätt, måste vi säkerställa att alla möjliga tillstånd och övergångar har beaktats i vår invariant. Det handlar också om att förstå att vissa initiala tillstånd kan vara ogiltiga om de inte uppfyller de nödvändiga villkoren för att systemet ska fungera korrekt.