Abstract System konfigurationsspråk används nu allmänt för att driva införandet och utvecklingen av stora datorinfrastrukturer. De flesta sådana språk är mycket informella, vilket gör det svårt att resonera om konfigurationer, och införa en viktig källa till misslyckande. Vi hävdar att en strängare inställning till utvecklingen och specificeringen av dessa språk kommer att bidra till att undvika dessa svårigheter och ge ett antal ytterligare fördelar. För att testa detta påstående presenterar vi en formell semantik för kärnan i SmartFrog konfigurationsspråk. Vi visar hur detta kan användas för att bevisa viktiga egenskaper såsom avslutande av sammanställningsprocessen. För att visa att detta också bidrar till den praktiska utvecklingen av tydliga och korrekta kompilatorer, presenterar vi tre oberoende implementeringar, och verifierar deras likvärdighet med varandra, och med semantiken. Med stöd av ett utökat exempel från ett verkligt konfigurationsscenario visar vi hur processen med att utveckla semantiken har förbättrat förståelsen av språket, lyft fram problemområden och föreslagit alternativa tolkningar. Detta leder oss att förespråka denna strategi för den framtida utvecklingen av praktiska konfigurationsspråk.
Anderson och Herry REF utvecklar en denotationssemantik för SmartFrog konfigurationsspråk som troget modellerar sin icke-deterministiska semantik.
A Formal Semantics for the SmartFrog Configuration Language