[ALL] Curiosita' sui flusso di controllo di un programma

[Unrue]

Originariamente inviato da cionci

Non è una cosa così rara.
Se vai a vedere software e sistemi operativi per sonde e veicoli spaziali, centrali nucleari e roba di questo tipo, il coverage della verifica formale deve raggiungere spesso il 95% del codice. Esistono linguaggi appositi per la verifica formale. Cose che fero86 non conosce perché ha tolto ingegneria del software dal suo piano di studi

Ciao,

potresti indicarmi qualche link in proposito? La cosa è molto interessante.

[cionci]

Originariamente inviato da Unrue

Ciao,

potresti indicarmi qualche link in proposito? La cosa è molto interessante.

Specifica formale, non verifica

Il già citato Linuguaggio Z (per l'esecuzione sequenziale), le reti di Petri/Petri estese (per la concorrenza), poi ci sono altri linguaggi specifici:
http://en.wikipedia.org/wiki/Specification_language
http://en.wikipedia.org/wiki/Petri_net (non ho trovato niente per quelle estese)

[WarDuck]

Un esempio di strumento per la verifica formale del codice (quantomeno per la parte procedurale) sono le triple di Hoare:

http://en.wikipedia.org/wiki/Hoare_logic

[Unrue]

Originariamente inviato da cionci

Specifica formale, non verifica

Il già citato Linuguaggio Z (per l'esecuzione sequenziale), le reti di Petri/Petri estese (per la concorrenza), poi ci sono altri linguaggi specifici:
http://en.wikipedia.org/wiki/Specification_language
http://en.wikipedia.org/wiki/Petri_net (non ho trovato niente per quelle estese)

Ma la specifica formale è fatta a livello algoritmico presumo. Cioè, riesco a dire se il mio algoritmo è matematicamente corretto. O si riesce a scovare anche errori di implementazione quali ad esempio memory leak per dirla alla C ?

[marco.r]

Originariamente inviato da Unrue

Ma la specifica formale è fatta a livello algoritmico presumo. Cioè, riesco a dire se il mio algoritmo è matematicamente corretto. O si riesce a scovare anche errori di implementazione quali ad esempio memory leak per dirla alla C ?

Si', ci sono anche quelli. In generale pero' si fa solo la verifica di condizioni particolari (e.g. memory leak, dereferenziazione di null pointers e sforamento di array ). Al JPL ci sono uno o anche due gruppi che lavorano sull'argomento e hanno fatto parecchia ricerca a riguardo, e svilupppato dei tool per l'analisi tanto di Java quando di C++. Quello per java e' stato rilasciato open source e lo trovi qua: http://javapathfinder.sourceforge.net/
Per la verifica formale di piu' alto livello al momento ci si "accontenta" di farlo su modelli piu' astratti definito in un qualche linguaggio apposito. L'idea e' che specifichi come deve comportarsi il programma e poi fai l'analisi del modello. Il problema e' che da un lato scrivere correttamente le specifiche diventa difficile quasi quanto scrivere il programma, e il modello non riflette necessariamente il programma vero e proprio.
Comunque e' un campo di ricerca in piena attivita' per cui mi aspetto che le cose migliorino col tempo.

[wingman87]

Originariamente inviato da cionci

Le discussioni sono state tutte copiate nella sezione Programmazione.

Temo che ormai sia tardi, ma non è che ci sia un modo per recuperare tutti i thread di Diamonds per raccoglierne i link in un unico thread?

[cionci]

Originariamente inviato da wingman87

Temo che ormai sia tardi, ma non è che ci sia un modo per recuperare tutti i thread di Diamonds per raccoglierne i link in un unico thread?

http://www.google.it/search?hl=it&sa...2&start=0&sa=N
http://www.google.it/search?hl=it&sa...g&start=0&sa=N

[tomminno]

Originariamente inviato da gugoXX

Non ho capito. In una ingegneria infomatica permettono di togliere dal piano di studi ingegneria del software?

Nell'indirizzo controlli numerici Ingegneria del Software non c'è. Altrimenti direi che è un esame obbligatorio.

[wingman87]

Originariamente inviato da cionci

http://www.google.it/search?hl=it&sa...2&start=0&sa=N
http://www.google.it/search?hl=it&sa...g&start=0&sa=N

Non ci avevo proprio pensato. Grazie!

[LUVІ]

Originariamente inviato da fero86

e il motivo per cui sono mancate le dita qual é? ricordo di aver letto dei post piuttosto eloquenti in merito!

Probabilmente che non si campa, con i diamonds! Anche se, da esterno, sembrava una cosa molto bella.
Scusate l'intrusione, ogni tanto vi leggo, per vedere quanto sarebbe bello poter lavorare ancora nel campo....

LuVi