Che cosa è “semantica formale”?

Question

Sto leggendo un documento molto stupido e si continua a parlare di come Giotto definisce una "semantica formale".

  

Giotto ha una semantica formale che specifica il significato di interruttori di modalità, di comunicazione intertask e della comunicazione con l'ambiente programma.

Sono sul bordo, ma proprio non riesco a capire che cosa intende per "semantica formale".

Answer 1

semantica formale descrivono la semantica in - bene, un modo formale - utilizzando la notazione che esprime il significato di cose in modo non ambiguo.

E 'l'opposto di informali la semantica, che è essenzialmente solo descrivendo tutto in inglese. Questo può essere più facile da leggere e capire, ma crea il potenziale di errori di interpretazione, che potrebbe portare a errori perché qualcuno non ha letto un paragrafo nel modo che intendeva di leggerlo.

Un linguaggio di programmazione può avere una semantica sia formali che informali - la semantica informali sarebbero quindi servire come un "testo semplice" spiegazione delle semantica formale, e la semantica formale sarebbe il posto dove guardare, se non siete sicuri di cosa la spiegazione informale significa veramente.

Answer 2

Per espandere sulla risposta di Michael Madsen un po ', un esempio potrebbe essere il comportamento dell'operatore ++. Informalmente, descriviamo l'operatore usando parole semplici. Per esempio:

  

Se x è una variabile di tipo int, ++x provoca x da incrementato di uno.

(sto assumendo che non integer overflow, e che ++x non restituisce nulla)

In una semantica formale (e ho intenzione di utilizzare la semantica operativa), avremmo un po 'di lavoro da fare. In primo luogo, abbiamo bisogno di definire una nozione di tipi. In questo caso, ho intenzione di assumere che tutte le variabili sono di tipo int. In questo semplice linguaggio, lo stato attuale del programma può essere descritto da un negozio, che è una mappatura dalle variabili ai valori. Ad esempio, ad un certo punto del programma, x potrebbe essere pari a 42, mentre y è uguale a -5351. L'archivio può essere utilizzata come una funzione -. Così, per esempio, se il s negozio ha la x variabile con il valore 42, quindi s(x) = 42

Sono inclusi anche allo stato attuale del programma è restanti dichiarazioni del programma che dobbiamo eseguire. Si può racchiudere questo come <C, s>, dove C è il programma rimanente e s è il negozio.

Quindi, se abbiamo il <++x, {x -> 42, y -> -5351}> Stato, questo è informalmente uno stato in cui il comando unico rimasto da eseguire è ++x, il x variabile ha valore 42, e il y variabile ha valore -5351.

Possiamo quindi definire le transizioni da uno stato del programma ad un altro - descriviamo cosa accade quando prendiamo il passo successivo del programma. Così, per ++, potremmo definire la seguente semantica:

<++x, s> --> <skip, s{x -> (s(x) + 1)>

Un po 'informale, eseguendo ++x, il comando successivo è skip, che non ha alcun effetto, e le variabili nel negozio sono invariati, ad eccezione di x, che ora ha il valore che originariamente aveva più uno. C'è ancora del lavoro da fare, come ad esempio definendo la notazione che ho usato per l'aggiornamento del negozio (che io non ho fatto per fermare questa risposta ottenere anche di più!). Quindi, una specifica istanza della norma generale potrebbe essere:

<++x, {x -> 42, y -> -5351}> --> <skip, {x -> 43, y -> -5351}>

Speriamo che ti dà l'idea. Si noti che questo è solo un esempio di semantica formale -. Insieme semantica operazionale, c'è la semantica assiomatiche (che spesso utilizza la logica di Hoare) e semantica denotazionale, e probabilmente molto altro che io non sono a conoscenza

Come ho già detto in un commento ad un'altra risposta, un vantaggio di semantica formale è che si possono usare per dimostrare alcune proprietà del programma, per esempio, che termina. Oltre a mostrare il vostro programma non presenta cattivo comportamento (come la non-terminazione), si può anche dimostrare che il vostro programma si comporta come richiesto dal dimostrando il vostro programma corrisponde a una determinata specifica. Detto questo, non ho mai trovato l'idea di specifica e la verifica di un programma di tutto ciò che convincente, dal momento che ho trovato la specifica di solito solo di essere riscritto il programma di logica, e così la specifica è altrettanto probabile che sia buggy.

Answer 3

Proprio come la sintassi di un linguaggio può essere descritto da una grammatica formale (ad esempio BNF ), è possibile utilizzare diversi tipi di formalismi per mappare che la sintassi di oggetti matematici (vale a dire il senso della sintassi).

Questa pagina da Un'introduzione pratica a denotazionale semantica è una bella introduzione a come [denotazionale] semantica riguarda la sintassi. L'inizio del libro fornisce anche una breve storia di altri, approcci non denotazionale a semantica formale (anche se il link wikipedia Michael dato va in ancor più in dettaglio, ed è probabilmente più up-to-date).

dell'autore sito :

  

I modelli per la semantica non hanno   catturati-on nella stessa misura in cui BNF   ed i suoi discendenti hanno in sintassi.   Ciò può essere perché la semantica fa   sembrano essere semplicemente più difficile di quanto   sintassi. Il sistema più efficace è   semantica denotazionale che descrive   tutte le caratteristiche che si trovano in un imperativo   linguaggi di programmazione e ha un suono   basi matematiche. (C'è ancora   ricerca attiva nei sistemi di tipo e   programmazione parallela.) Molti   le definizioni possono essere denotazionale   eseguito come interpreti o tradotta   in "compilatori", ma questo non è ancora   portato a generatori di efficiente   compilatori che può essere un altro motivo   che la semantica denotazionale è meno   popolare di BNF.

Answer 4

Che cosa si intende, nel contesto di un linguaggio di programmazione come Giotto è, che una lingua con semantica formale, ha un matematicamente rigoroso interpretazione dei suoi singoli costrutti del linguaggio.

La maggior parte dei linguaggi di programmazione di oggi non sono rigorosamente definiti. Possono aderire a documenti standard che sono abbastanza dettagliata, ma è in ultima analisi, la responsabilità del compilatore di emettere codice che in qualche modo aderisce a tali documenti standard.

Un linguaggio formalmente indicato d'altra parte è normalmente utilizzato quando è necessario fare un ragionamento sul codice programma utilizzando, per esempio, il model checking o teoremi. Linguaggi che si prestano a queste tecniche tendono ad essere quelli funzionali, come ML o Haskell, poiché questi sono definiti utilizzando funzioni matematiche e trasformazioni tra loro; vale a dire, i fondamenti della matematica.

C o C ++ d'altra parte sono informalmente definite da descrizioni tecniche, anche se esistono documenti accademici che formalizzano gli aspetti di queste lingue (ad esempio, Michael Norrish: una semantica formale per C ++, https://publications.csiro.au/rpr/pub?pid=nicta:1203 ), ma che spesso non trovano la loro strada nelle norme ufficiali (forse a causa della mancanza di praticità, esp. difficoltà a mantenere).