|
Categorie
Winzipedia Uso dell'wiki |
DesignByContractInformatica3.DesignByContract VersioniNascondi le modifiche minori - Mostra le modifiche Modificata la linea 19: da:
* L'utilizzatore, o cliente, si impegna a rispettare le condizioni per il corretto utilizzo del software che sono scritte nel contratto (per esempio che gli input siano corretti o all'interno di un certo range). Queste condizioni sono chiamate '''precondizioni''' e sono solitamente decise da scrive il software. a:
* L'utilizzatore, o cliente, si impegna a rispettare le condizioni per il corretto utilizzo del software che sono scritte nel contratto (per esempio che gli input siano corretti o all'interno di un certo range). Queste condizioni sono chiamate '''precondizioni''' e sono solitamente decise da chi scrive il software. Modificate le linee 2-4: da:
'''Autori:''' [[Profiles.Vincenzo|Vincenzo Manzoni]] '''Hanno contribuito:''' a:
'''Autori:''' [[Profiles.Vincenzo|Vincenzo Manzoni]], [[Profiles.Andrea|Andrea Rota]]\\ Modificate le linee 6-7: da:
->[-Introduzione al Design by contract come di progettazione del software.-] a:
->[-Introduzione al Design by contract come di progettazione del software. Nell'articolo saranno anche introdotti alcuni linguaggi specifici per il Dbc.-] Modificata la linea 58: da:
* descrizione accurata di che si intende per ''comportamento corretto'' di un programma, utile in fase di testing: diremo che un programma ''A'' corretto se partendo da uno stato che soddisfa il predicato ''P'' delle precondizioni si arriva ad uno stato che soddisfa il predicato ''Q'' delle postcondizioni (Hoare Triple, v. Risorse in rete) a:
* descrizione accurata di che si intende per ''comportamento corretto'' di un programma, utile in fase di testing: diremo che un programma ''A'' corretto se partendo da uno stato che soddisfa il predicato ''P'' delle precondizioni si arriva ad uno stato che soddisfa il predicato ''Q'' delle postcondizioni (Hoare Triple, v. Risorse in rete); Aggiunte le linee 61-65:
A questi si aggiungono anche dei vantaggi tecnici non indifferenti: * Sviluppo diventa maggiormente focalizzato sulle specifiche * Il dbc fornisce quasi automaticamente piani di test per ''black-box'' * I malfunzionamenti vengono individuati vicino alla loro causa, che facile individuare i difetti del software e correggerli. Modificate le linee 125-126: da:
Gli svantaggi delle JDK Assertion che non dispongono di una semantica propria (se non quella mutuata da Java), non sono visibili direttamente dall'interfaccia e non possibile distinguere se una assert riguarda una precondizione, una postcondizione o un invariante. a:
Gli svantaggi delle JDK Assertion che non dispongono di una semantica propria (se non quella mutuata da Java), non sono visibili direttamente dall'interfaccia e non possibile distinguere se una assert riguarda una precondizione, una postcondizione o un invariante. Le JDK Assertion inoltre non dispongono di un meccanismo di documentazione. 14/06/2006 ore 16:22 CEST
di - Aggiunta link interessanti
Aggiunte le linee 125-126:
* Eiffel Software, http://www.eiffel.com/, la casa produttrice dei tool basati sul linguaggio Eiffel * GNU Nana Project, http://www.gnu.org/software/nana/nana.html, il sito ufficiale delle librerie Nana per GNU C e C++. 14/06/2006 ore 16:19 CEST
di - Aggiunto Gnu Nana
Modificate le linee 65-81: da:
a:
GNU Nana una libreria libera che fornisce un supporto al controllo delle asserzioni e al logging per i compilatori GNU C e GNU C++. Fornisce l'implementazione di alcune idee di Eiffel, VDM, Z e Anna in GNU C/C++. [-(Liberamente tradotto da http://www.gnu.org/software/nana/nana.html)-] '''Esempio''' Sia @@square_root@@ una funzione intera che ritorna la radice quadrata arrotondata all'intero basso di un numero intero x. int square_root(int x) /*@ assume x>0; return y>0, y<=x*x, y<(x+1)*(x+1); @*/ dove @@assume@@ indica una precondizione e @@return@@ indica una postcondizione. Modificate le linee 83-84: da:
Vedere l'[[informatica3.JML|articolo JML]] di [[profiles.Giorgio|Giorgio]] e [[profiles.Vincenzo|Vincenzo]] a:
Vedere l'[[informatica3.JML|articolo JML]] di [[profiles.Giorgio|Giorgio]] e [[profiles.Vincenzo|Vincenzo]]. Aggiunte le linee 64-68:
!!!Gnu Nana !!!JML Vedere l'[[informatica3.JML|articolo JML]] di [[profiles.Giorgio|Giorgio]] e [[profiles.Vincenzo|Vincenzo]] 14/06/2006 ore 15:59 CEST
di - Finito
Aggiunta la linea 77:
Aggiunta la linea 81:
Modificate le linee 87-88: da:
a:
Permettono di ''annegare'' nel codice Java dei controlli che vengono eseguiti a runtime: la sintassi : assert(condizioni) ad esempio public int fattoriale(int n) { assert(n>0); ... } Se le condizioni non si verificano l'assert fallisce: differentemente dalle eccezioni, il meccanismo delle JDK Assertion essere spento quando si ha sufficiente fiducia nel codice: in questo modo il codice viene eseguito rapidamente. Gli svantaggi delle JDK Assertion che non dispongono di una semantica propria (se non quella mutuata da Java), non sono visibili direttamente dall'interfaccia e non possibile distinguere se una assert riguarda una precondizione, una postcondizione o un invariante. Cancellate le linee 102-104:
!! Da fare # Proseguire nella stesura dell'articolo, io ho utilizzato le slide del 2005 che sono uguali a quelle di quest'anno, a meno di Jass. Modificate le linee 11-12: da:
Cosa un contratto? a:
!!!Cosa un contratto? Un contratto un ''accordo tra un cliente e un contrattore (o fornitore)''. Il contratto ha alcune : Modificate le linee 65-66: da:
a:
E' un vero e proprio linguaggio di programmazione che contiene istruzioni per la gestione delle precondizioni, delle post condizioni e degli invarianti. Ecco un esempio: -- classe che modella un conto bancario class CONTOBANCARIO : INTEGER _min: INTEGER is 1000 -- costruttore make (versamento_iniziale: INTEGER) is do :=versamento_iniziale end -- precondizioni sul costruttore require pre1: versamento_iniziale>=_min -- postcondizioni sul costruttore ensure post1: =versamento_iniziale Modificate le linee 32-33: da:
La domanda che un programmatore si pone spesso : "Devo controllare che gli input passati dall'utente siano corretti?". La risposta che la tecnica DBC : "No, il controllo delle precondizioni del cliente". a:
La domanda che un programmatore si pone spesso : "Devo controllare che gli input passati dall'utente siano corretti?". La risposta che la tecnica DBC : "No, il controllo delle precondizioni del cliente". Nel caso presentato nell'esempio precedente, il cliente avrebbe dovuto scrivere: if(numero>=0){ fattNumero = fattoriale(numero); } else { // azione di segnalazione/correttiva printf("Il numero inserito negativo!"); } Modificate le linee 22-23: da:
a:
Aggiunte le linee 25-27:
Sostanzialmente la stipula del contratto aiuta il programmatore a ridurre la dei casi d'uso del suo software, sgravandolo da qualora il suo prodotto sia usato non correttamente e aiuta il cliente ad usare correttamente il software. La scrittura dei vincoli viene fatta usando predicati logici. Modificata la linea 48: da:
* descrizione accurata di che si intende per ''comportamento corretto'' di un programma, utile in fase di testing: diremo che un programma ''A'' corretto se partendo da uno stato che soddisfa il predicato ''P'' delle precondizioni si arriva ad uno stato che soddisfa il predicato ''Q'' delle postcondizioni (Hoare Triple, v. Risorse in rete). a:
* descrizione accurata di che si intende per ''comportamento corretto'' di un programma, utile in fase di testing: diremo che un programma ''A'' corretto se partendo da uno stato che soddisfa il predicato ''P'' delle precondizioni si arriva ad uno stato che soddisfa il predicato ''Q'' delle postcondizioni (Hoare Triple, v. Risorse in rete). Modificata la linea 48: da:
* descrizione accurata di che si intende per ''comportamento corretto'' di un programma, utile in fase di testing: diremo che un programma ''A'' corretto se partendo da uno stato che soddisfa il predicato ''P'' delle precondizioni si arriva ad uno stato che soddisfa il predicato ''Q'' delle postcondizioni (Hoare Triple, v. Risorse in rete). a:
* descrizione accurata di che si intende per ''comportamento corretto'' di un programma, utile in fase di testing: diremo che un programma ''A'' corretto se partendo da uno stato che soddisfa il predicato ''P'' delle precondizioni si arriva ad uno stato che soddisfa il predicato ''Q'' delle postcondizioni (Hoare Triple, v. Risorse in rete). {$ {P}A{Q} $} Modificate le linee 52-54: da:
Esistono vari linguaggi che permettono di usare tecniche DBC per la modellazione e la scrittura del codice; fra questi ricordiamo '''Gnu Nana''', '''Jml''', '''Eiffel''' e le '''JDK assertion a:
Esistono vari linguaggi che permettono di usare tecniche DBC per la modellazione e la scrittura del codice; fra questi ricordiamo '''Gnu Nana''', '''Jml''', '''Eiffel''' e le '''JDK 1.4 assertions'''. Modificata la linea 52: da:
Esistono vari linguaggi che permettono di usare tecniche DBC per la modellazione e la scrittura del codice; fra questi ricordiamo '''Gnu Nana''', '''Jml''', '''Eiffel''' e le '''JDK a:
Esistono vari linguaggi che permettono di usare tecniche DBC per la modellazione e la scrittura del codice; fra questi ricordiamo '''Gnu Nana''', '''Jml''', '''Eiffel''' e le '''JDK 14 Modificata la linea 26: da:
'''Esempio''' a:
'''Esempio'''\\ Aggiunte le linee 38-43:
!!! Postcondizioni Le postcondizioni vanno valutate ''esclusivamente'' alla fine della computazione. !!! Invarianti Sono condizioni che devono valere dalla creazione dell'oggetto alla sua morte e sono riferite a caratteristiche dell'oggetto. Ad esempio se l'oggetto un orologio, il contatore delle ore essere compreso fra 0 e 23 e il contatore dei minuti fra 0 e 59. Modificate le linee 47-48: da:
* il programmatore concentrarsi sul problema da risolvere e non sul controllo della correttezza degli input (che essere fatto ad uno stadio successivo) a:
* il programmatore concentrarsi sul problema da risolvere e non sul controllo della correttezza degli input (che essere fatto ad uno stadio successivo); * descrizione accurata di che si intende per ''comportamento corretto'' di un programma, utile in fase di testing: diremo che un programma ''A'' corretto se partendo da uno stato che soddisfa il predicato ''P'' delle precondizioni si arriva ad uno stato che soddisfa il predicato ''Q'' delle postcondizioni (Hoare Triple, v. Risorse in rete). Aggiunte le linee 51-60:
!! Linguaggi per il DBC Esistono vari linguaggi che permettono di usare tecniche DBC per la modellazione e la scrittura del codice; fra questi ricordiamo '''Gnu Nana''', '''Jml''', '''Eiffel''' e le '''JDK 1.4 assertion'''. !!!Eiffel !!!JDK 1.4 Assertion Modificate le linee 62-63: da:
Wikipedia ha una voce relativa al [[http://en.wikipedia.org/wiki/Design_by_contract|Design By Contract]], con un elenco dei tool per i vari linguaggi. a:
* Wikipedia ha una voce relativa al [[http://en.wikipedia.org/wiki/Design_by_contract|Design By Contract]], con un elenco dei tool per i vari linguaggi. * Un'interessante pagina di Wikipedia sulla [[http://en.wikipedia.org/wiki/Hoare_logic|Hoare logic]], argomento fortemente connesso con il DBC e il testing. Modificata la linea 66: da:
# Proseguire nella stesura dell'articolo, io ho utilizzato le slide del 2005 che sono uguali a quelle di quest'anno, a meno di a:
# Proseguire nella stesura dell'articolo, io ho utilizzato le slide del 2005 che sono uguali a quelle di quest'anno, a meno di Jass. Modificate le linee 3-4: da:
'''Hanno contribuito: [[Profiles.Andrea|Andrea Rota]] a:
'''Hanno contribuito:''' [[Profiles.Andrea|Andrea Rota]] Modificata la linea 48: da:
# a:
# Proseguire nella stesura dell'articolo, io ho utilizzato le slide del 2005 che sono uguali a quelle di quest'anno, a meno di Jass Modificate le linee 29-30: da:
a:
!!! Precondizioni La domanda che un programmatore si pone spesso : "Devo controllare che gli input passati dall'utente siano corretti?". La risposta che la tecnica DBC : "No, il controllo delle precondizioni del cliente". Le precondizioni possono essere o meno restrittive; ecco un breve elenco di esempi di vincoli ordinati per : # @@TRUE@@: nessuna precondizione. Il funzionamento corretto del software garantito per ogni input. # @@n>0@@: precondizione intervallare. Il funzionamento corretto del software garantito solo per i valori di input interni all'intervallo. # @@n=1 or n=3@@: precondizione puntuale. Il vincolo sugli input ristretto a singoli valori di input. # @@FALSE@@: il funzionamento corretto non viene garantito per nessun input. Modificate le linee 19-23: da:
* L'utilizzatore, o cliente, si impegna a rispettare le condizioni per il corretto utilizzo del software che sono scritte nel contratto (per esempio che gli input siano corretti o all'interno di un certo range). Queste condizioni sono chiamate '''precondizioni''' * Il programmatore, o fornitore, si impegna l'output del suo Sostanzialmente la stipula del contratto aiuta il programmatore a ridurre la dei casi d'uso del suo a:
* L'utilizzatore, o cliente, si impegna a rispettare le condizioni per il corretto utilizzo del software che sono scritte nel contratto (per esempio che gli input siano corretti o all'interno di un certo range). Queste condizioni sono chiamate '''precondizioni''' e sono solitamente decise da scrive il software. * Il programmatore, o fornitore, si impegna l'output del suo software rispetti le condizioni che sono scritte nel contratto, il cliente abbia rispettato tutti i vincoli nell'uso del prodotto. Queste condizioni sono chiamate '''postcondizioni''' e sono solitamente decise da chi commissiona e usa il software. Sostanzialmente la stipula del contratto aiuta il programmatore a ridurre la dei casi d'uso del suo software, sgravandolo da qualora il suo prodotto sia usato non correttamente e aiuta il cliente ad usare correttamente il software. Gli obblighi del cliente diventano vantaggi per il fornitore e viceversa. Modificate le linee 29-44: da:
Un contratto costituito da '''precondizioni''' e '''postcondizioni'''. Le precondizioni vengono decise da chi scrive il metodo che, in generale, non deve gestire ogni input (il quale quindi essere specificato). Il cliente deve garantire questa con controlli appropriati. !!! Esempio Se @@pre@@ la precondizione per un metodo @@m@@, all'interno del cliente deve comparire un codice che si comporti come questo: if( x.pre ) x.m(); else // statement Il fornitore deve garantire che le postcondizioni nell'implementazione del metodo. Gli obblighi del cliente diventano vantaggi per il fornitore e viceversa. a:
02/06/2006 ore 12:22 CEST
di - Aggiornamento con le slide
Modificate le linee 3-4: da:
'''Hanno contribuito:''' a:
'''Hanno contribuito: [[Profiles.Andrea|Andrea Rota]]''' Modificate le linee 18-19: da:
L'oggetto del contratto per noi il ''software''; il contratto essere stipulato sulla classe o sul singolo metodo. a:
L'oggetto del contratto per noi il ''software''; il contratto essere stipulato sulla classe o sul singolo metodo. Stipulare un contratto sul software significa crare un doppio vincolo fra chi scrive il software e chi lo utilizza. * L'utilizzatore, o cliente, si impegna a rispettare le condizioni per il corretto utilizzo del software che sono scritte nel contratto (per esempio che gli input siano corretti o all'interno di un certo range). Queste condizioni sono chiamate '''precondizioni'''. * Il programmatore, o fornitore, si impegna l'output del suo software rispetti le condizioni che sono scritte nel contratto, il cliente abbia rispettato tutti i vincoli nell'uso del prodotto. Queste condizioni sono chiamate '''postcondizioni'''. Sostanzialmente la stipula del contratto aiuta il programmatore a ridurre la dei casi d'uso del suo software, sgravandolo da qualora il suo prodotto sia usato non correttamente. !!!Esempio Il contratto prevede che il metodo @@int fattoriale(n)@@ accetti numeri positivi e restituisca la funzione n!. Il cliente si impegna a passare n positivo e il fornitore a calcolare il fattoriale correttamente. Se il numero passato n negativo, il fornitore non tenuto a nessuna garanzia sulla correttezza dei risultati. Aggiunta la linea 46:
* il programmatore concentrarsi sul problema da risolvere e non sul controllo della correttezza degli input (che essere fatto ad uno stadio successivo) 01/06/2006 ore 21:25 CEST
di - Correzione di grammatica
Modificata la linea 45: da:
# Integrare con le slide di Gargantini quando le ; questo articolo l'ho scritto prendendo le informazioni dagli appunti a:
# Integrare con le slide di Gargantini quando le ; questo articolo l'ho scritto prendendo le informazioni dagli appunti di Giorgio. 01/06/2006 ore 21:22 CEST
di - Vantaggi e svantaggi; da fare.
Aggiunte le linee 34-40:
Gli obblighi del cliente diventano vantaggi per il fornitore e viceversa. !! Vantaggi nell'utilizzo dei contratti Esistono dei vantaggi nell'utilizzo dei contratti: * le classi vengono documentate in modo accurato e questo favorisce la del software; * se cliente e fornitore rispettano i contratti, viene garantita maggiormente la correttezza del software. Modificate le linee 42-45: da:
Wikipedia ha una voce relativa al [[http://en.wikipedia.org/wiki/Design_by_contract|Design By Contract]], con un elenco dei tool per i vari linguaggi. a:
Wikipedia ha una voce relativa al [[http://en.wikipedia.org/wiki/Design_by_contract|Design By Contract]], con un elenco dei tool per i vari linguaggi. !! Da fare # Integrare con le slide di Gargantini quando le ; questo articolo l'ho scritto prendendo le informazioni dagli appunti del Giorgio. 01/06/2006 ore 21:15 CEST
di - Aggiunta di precondizioni e postcondizioni
Modificate le linee 11-12: da:
a:
* lega tra di loro '''due''' parti, cliente e fornitore; * specifica ''obblighi'' e ''benefici'' per entrambe le parti; * non contiene clausole nascoste. !! Precondizioni e postcondizioni !!! Esempio if( x.pre ) x.m(); else // statement Il fornitore deve garantire che le postcondizioni nell'implementazione del metodo. 01/06/2006 ore 21:04 CEST
di - Creazione della pagina
Aggiunte le linee 1-14:
!Design by contract '''Autori:''' [[Profiles.Vincenzo|Vincenzo Manzoni]]\\ '''Hanno contribuito:''' ->'''Sommario''' ->[-Introduzione al Design by contract come di progettazione del software.-] !!Introduzione Il '''Design by contract''' (o brevemente DBC) una particolare per la progettazione del software, che vede al centro un ''contratto'' tra un "cliente" e un "fornitore". Cosa un contratto? Un contratto un ''accordo tra un cliente e un contrattore (o fornitore)''. !! Risorse in rete Wikipedia ha una voce relativa al [[http://en.wikipedia.org/wiki/Design_by_contract|Design By Contract]], con un elenco dei tool per i vari linguaggi. |