AA 2016-2017 10. Il debugging di...

32
10. Il debugging di astrazioni AA 2016-2017 1

Transcript of AA 2016-2017 10. Il debugging di...

Page 1: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

10.IldebuggingdiastrazioniAA2016-2017

1

Page 2: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Astrazionisuida3:specifica

  Ingredien33picidiunaastrazionesuida3  Uninsiemediastrazioniproceduralichedefinisconotu?imodiperu3lizzareuninsiemedivalorio  Creareo  Manipolareo  Osservare

  CreatorieproduDori:meccanismiprimi3via?allaprogrammazionedelladefinizionedinuovivalori

  Mutator:modificanoilvalore(manonhannoeffeDosu==,nonoperanopereffe?laterali)

  Osservatori:strumentolinguis3coperselezionarevalori

2

Page 3: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Implementazionevs.Specifica

Representa)onInvariant:Object→booleano  Stabilisceseunaistanzaèbenformatao  Stabiliscel’insiemeconcretodeivaloridell’astrazione(ovveroquelli

chesonounaimplementazionedeivaloriastra?)o  Guidaperchiimplementa/modifica/verifical’implementazionedelle

astrazioni:nessunogge@odeveviolarerepinvariantAbstrac)onFunc)on:Object→abstractvalue

o  StabiliscecomeinterpretarelastruDurada3concretadellaimplementazione

o  ÈdefinitasolamentesuivaloricherispeDanol’invariantedirappresentazione

o  Guidaperchiimplementa/modifical’astrazione:ognioperazionedevefare“lacosagiusta”conlarappresentazioneconcreta

3

Page 4: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Esempio:CharSet

// Overview: CharSet insieme finito modificabile di // Characters

// @effects: crea un CharSet nuovo e vuoto public CharSet( ) {...}

// @modifies: this // @effects: thispost = thispre U {c} public void insert(Character c) {...}

// @modifies: this // @effects: thispost = thispre \ {c} public void delete(Character c) {...}

// @effects: return (c ∈ this) public boolean member(Character c) {...}

// @effects: return cardinalita’ di this (this.size( )) public int size( ) {...}

4

Page 5: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

CharSet:implementazione?

class CharSet { private List<Character> elts =

new ArrayList<Character>( );

public void insert(Character c) { if (elts.add(c)){return;}

} public void delete(Character c) {

int i = elts.indexOf(c); if (i > -1) elst.remove(i); } public boolean member(Character c) {

return elts.contains(c); } public int size( ) {

return elts.size( ); } }

5

Page 6: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

CharSet:implementazione?

class CharSet { private List<Character> elts =

new ArrayList<Character>( );

public void insert(Character c) { if (elts.add(c)){return;}

} public void delete(Character c) {

int i = elts.indexOf(c); if (i > -1) elst.remove(i); } public boolean member(Character c) {

return elts.contains(c); } public int size( ) {

return elts.size( ); } }

6

Doveènascostol’errore?

Page 7: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

class CharSet { private List<Character> elts =

new ArrayList<Character>( );

public void insert(Character c) { if (elts.add(c)){return;}

} public void delete(Character c) {

int i = elts.indexOf(c); if (i > -1) elst.remove(i); } public boolean member(Character c) {

return elts.contains(c); } public int size( ) {

return elts.size( ); } }

7

CharSet s = new CharSet( ); Character a = new Character('a'); s.insert(a); s.insert(a); s.delete(a); if (s.member(a)) System.out.print("wrong"); else System.out.print("right");

CharSet:implementazione?

Page 8: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

class CharSet { private List<Character> elts =

new ArrayList<Character>( );

public void insert(Character c) { if (elts.add(c)){return;}

} public void delete(Character c) {

int i = elts.indexOf(c); if (i > -1) elst.remove(i); } public boolean member(Character c) {

return elts.contains(c); } public int size( ) {

return elts.size( ); } }

8

Doveènascostol’errore?

CharSet s = new CharSet( ); Character a = new Character('a'); s.insert(a); s.insert(a); s.delete(a); if (s.member(a)) System.out.print("wrong"); else System.out.print("right");

CharSet:implementazione?

Page 9: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Cerchiamol’errore

  Primotenta5vo:deleteèsbagliatao  controllal’appartenenzamarimuovetuDeleoccorrenze?

  Secondotenta5vo:insertèsbagliatao  nondovrebbeinserireuncaraDerequandoègiàpresente

  Comeoperiamo?o  u3lizziamorepresenta3oninvariantpermuovercieeliminarel’erroreo  ilcodicebendocumentatoeglistrumen3dispecificaformaleci

aiutanonell’operazionediindividuazioneerimozionedell’errore

9

Page 10: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Invariantedirappresentazione  class CharSet { // Rep invariant: // elts non contiene elementi null e non // contiene duplicati private List<Character> elts = ... ...

Possiamoscriverloancheformalmente(conglistrumen3diLPP): ∀ indice i di elts . elts.elementAt(i) ≠ null ∀ indice i, j di elts . i ≠ j ⇒ ¬ elts.elementAt(i).equals(elts.elementAt(j)) Notare che ArrayList ammette null !!!

10

Page 11: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Oralocalizziamol’errore

// Rep invariant: // elts: no null e no duplicati public void insert(Character c) { if (elts.add(c)){return;}

} public void delete(Character c) { int i = elts.indexOf(c);

if (i > -1) elst.remove(c); }

11

Page 12: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Comesifaildebugging

L’ideacheintendiamoperseguireèlaseguente:

Proge:atedelcodiceinmodotalechetu:eleoperazionidi“bug-checking”sianoimplementateu5lizzandocomeguidal’invariantedi

rappresentazione

12

Page 13: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Verificadelrepinvariant

Ideaderivatadalletecnichediprova:controllareingressoeuscitadaimetodi

public void delete(Character c) { checkRep( ); // alternativa: invocare repOK( )

int i = elts.indexOf(c); if (i > -1) elst.remove(c); // Come garantire che venga sempre invocata? // (usiamo un blocco finally) checkRep( ); } ... /** elts no duplicati. */ private void checkRep( ) { ... }

13

Page 14: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

defensiveprogramming

  Assunzione:programmareèunprocessodi3po“trialanderror”

  ProgeDaredelcodiceinmodotalecheo  allachiamatadeimetodi

! verificarepinvariant! verificapre-condizioni

o  all’uscitadelmetodo! verificarepinvariant! verificapost-condizioni

  Verificarerepinvariant=verificarelapresenzadierrori

  Ragionaresulrepinvariant=evitaredifareerrori

14

Page 15: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

SempreCharSet

AggiungiamounmetodoaCharSet

// restituisce una lista degli elementi che // appartengono a this. public List<Character> getElts( );

Implementazione

// Rep invariant: elts no null e no dupl. public List<Character> getElts( ) { return elts; }

L’implementazionedigetEltspreservarepinvariant?

Mah?!….

15

Page 16: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Esporrelarappresentazione

Consideriamouncliente(semprediCharSet)CharSet s = new CharSet( ); Character a = new Character('a'); s.insert(a); s.getElts( ).add(a); // usiamo add in modo liberale s.delete(a); if (s.member(a)) ...

 AbbiamounaesposizionedellarappresentazioneconunaccessoindireDo(tramiteilmetodogetElts)

 Problema:bugdaevitareo  progeDarel’astrazioneinmododaevitarequestoproblemao  progeDaredeitestconclien3“malevoli”:usarevalorimutabilipercapire

cosaavvieneneldeDaglio

16

Page 17: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Comesievita?

  Perevitarel’esposizionedellarappresentazioneunaprimatecnicaèquelladifarecopiedeida3cheoltepassonolabarrieradell’astrazioneo  copiain[parametrichediventanovaloridellarappresentazione]o  copiaout[risulta3chesonopartedell’implementazione]

  Esempio:PointADTmodificabile

class Line { private Point s, e; public Line(Point s, Point e) { this.s = new Point(s.x,s.y); this.e = new Point(e.x,e.y); } public Point getStart( ) { return new Point(this.s.x,this.s.y); } ...

}

17

Page 18: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

deepcopying

Unacopiashallow(operazionisuipuntatori)nonèsufficienteacausadell’aliasing!!!

Analizzarequestocodiceclass PointSet { private List<Point> points = ...

public List<Point> getElts( ) { return new ArrayList<Point>(points);

} }

18

Page 19: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Unasecondasoluzione

  UsarestruDureda3nonmodificabili

  Esempio:Point(nonmodificabile) class Line { private Point s, e; public Line(Point s, Point e) {

this.s = s; this.e = e;

} public Point getStart( ) {

return this.s; } ...

19

Page 20: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

StruDurenonmodificabili

  Vantaggio  l’aliasingnonèunproblemao  nonènecessariofarecopieo  repinvariantnonpuòessere“roDo”

  RichiedetuDaviasceltediprogrammazionedifferen3void raiseLine(double deltaY) { this.s = new Point(s.x, s.y+deltaY); this.e = new Point(e.x, e.y+deltaY);

}

  Classiimmutabilinellalibreria:String,Character,Integer,...

20

Page 21: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

AncorailcasogetElts

class CharSet { // rep invariant: elts: no null e no dupl. private List<Character> elts = ...

// returns: elts nell’insieme corrente public List<Character> getElts( ) {

return new ArrayList<Character>(elts); //copy out } ... }

21

Page 22: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Alterna3ve

// returns: ... public List<Character> getElts( ) { // versione 1 return new ArrayList<Character>(elts); //copy out! }

public List<Character> getElts( ) { // versione 2 return Collections.unmodifiableList<Character>(elts); }

JavaDoc:Collections.unmodifiableList:Returnsanunmodifiableviewofthespecifiedlist.Thismethodallowsmodulestoprovideuserswith"read-only"accesstointernallists.Queryopera5onsonthereturnedlist"readthrough"tothespecifiedlist,anda:emptstomodifythereturnedlist…resultinanUnsupportedOperationException.

22

Page 23: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Somegoodnews

public List<Character> getElts( ) { // versione 2 return Collections.unmodifiableList<Character>(elts); }

o iclien3nonpossonospezzareilrepinvarianto selalistaèdidimensionielevateèpiùefficientedellatecnicadelcopyouto siusanolibreriestandard(sempreunabuonacosa)

23

Page 24: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Somebadnews

public List<Character> getElts( ) { // versione 1 return new ArrayList<Character>(elts);//copy out! }

public List<Character> getElts( ) { // versione 2 return Collections.unmodifiableList<Character>(elts); }Ledueimplementazionisonodifferen3!!!

o entrambepermeDonodievitaredirompereilrepinvarianto entramberes3tuisconounalistadielemen3

Ma... xs = s.getElts( ); s.insert('a'); xs.contains('a');

Laversione2permeDediosservarelarappresentazione!!

24

Page 25: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Implementazionevs.Specifica

Representa)onInvariant:Object→booleano  Stabilisceseunaistanzaèbenformatao  Stabiliscel’insiemeconcretodeivaloridell’astrazione(ovveroquelli

chesonounaimplementazionedeivaloriastra?)o  Guidaperchiimplementa/modifica/verifical’implementazionedelle

astrazioni:nessunogge@odeveviolare

Abstrac)onFunc)on:Object→abstractvalueo  StabiliscecomeinterpretarelastruDurada3concretadella

implementazioneo  ÈdefinitasolamentesuivaloricherispeDanol’invariantedi

rappresentazioneo  Guidaperchiimplementa/modifical’astrazione:ognioperazione

devefare“lacosagiusta”conlarappresentazioneconcreta

25

Page 26: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Repinv.vincolalastruDura

Implementazionediinsertchepreservarepinvariantpublic void insert(Character c) { Character cc = new Character(encrypt(c)); if (!elts.contains(cc)) elts.addElement(cc); } public boolean member(Character c) { return elts.contains(c); }

Ilprogrammapresentadeicomportamen3nonadegua3

26

Page 27: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Repinv.vincolalastruDura

Implementazionediinsertchepreservarepinvariantpublic void insert(Character c) { Character cc = new Character(encrypt(c)); if (!elts.contains(cc)) elts.addElement(cc); } public boolean member(Character c) { return elts.contains(c); }

Ilprogrammapresentadeicomportamen3nonadegua3

27

CharSet s = new CharSet( ); s.insert('a'); if (s.member('a')) ...

Page 28: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Lafunzionediastrazione(AF)

Laabstrac3onfunc3onassocialarappresentazioneconcretaaivaloriastra?AF:Object→abstractvalueAF(CharSetthis)={c|cappar3eneathis.elts}

“insiemedeicaraDeriinthis.elts”o  nonèeseguibile:èun“valore”conceDualedellaastrazioneo  tuDavia,lafunzionediastrazionecipermeDediragionaresulle

modalitàconlequaliimetodioperanointerminidellavisioneastraDa(chehannoiclien3)

28

Page 29: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Ilcasoinsert

Laspecificadiinsert// modifies: this // effects: thispost = thispre U {c} public void insert (Character c) {…}

LaAFcidiceeffe?vamentecosasignificailrepinvariantAF(CharSetthis)={c|cappartenen3athis.elts}

Invochiamoinsert

All’ingressodelmetodovaleAF(thispre)≈eltspreAll’uscitaAF(thispost)=AF(thispre)U{encrypt('a')}

MegliousarequestaAFalterna3va

AF(this)={c|encrypt(c)appartenen3athis.elts}={decrypt(c)|cappartenen3athis.elts}

29

Page 30: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Esempio:AFperStack

30

new() 0 0 0

push(17) 17 0 0

Top=1

push(-9) 17 -9 0

Top=2

Top=0

stack=<>

stack=<17>

stack=<17,-9>

pop() 17 -9 0

stack=<17>Top=1

Sta3astra?stack=<17>=<17>

Sta3concre3

<[17,0,0], top=1> ≠

<[17,-9,0], top=1>

AFèunafunzioneL’inversodiAFnonloè

Page 31: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

31

Page 32: AA 2016-2017 10. Il debugging di astrazionipages.di.unipi.it/ferrari/CORSI/PR2/LEZIONI2017/PR2010.pdf · o i clien3 non possono spezzare il rep invariant o se la lista è di dimensioni

Riassuntofinale

Repinvarianto  Qualisonoivaloriconcre3cherappresentanovaloriastra?

Abstrac3onfunc3ono  Perognivaloreconcretores3tuisceilcorrispondentevaloreastraDo

Obie?vocomune:sonoentrambeindispensabilipercontrollarela

correDezzadell’astrazioneDisolito,ladocumentazionefavederesolamenteilrepinvariant

32