Ingegneria del software

Astrazioni funzionali e procedurali

6 minuti

Note

Un’astrazione procedurale, definisce, tramite una specifica, un’operazione complessa su dati generici (o parametrici).

Specifica

Una specifica è una descrizione di un’entità che prescinde dall’implementazione. Nel nostro caso è un astrazione del frammento di codice, e rappresenta la classe d’equivalenza di tutte le implementazioni possibili.

In Java la signature di un metodo ne esprime la sintassi, tuttavia non ci dice nulla circa la semantica. È vantaggiosa poiché:

  • L’implementazione può essere letta o scritta senza la necessità di analizzare le implementazioni di altre astrazioni.
  • L’astrazione può essere re-implementata senza effetti sulle astrazioni che la usano.

È data usando un linguaggio naturale o una semplice notazione matematica.

Java Modelling Language

Note

Java Modelling Language (JML) è un linguaggio formale di specifica basato su Java, non eseguibile dal compilatore. Le sue asserzioni possono:

  • Predicare su variabili
  • Quantificare su variabili
  • Invocare metodi puri
  • Predicare sull’invarianza di alcune variabili
  • Predicare sul corretto lancio delle eccezioni

Le specifiche JML sono aggiunte al codice Java tramite commenti, che cominciano con il simbolo @:

//@ <JML Specification>

/*@ <JML Specification> @*>

Funziona definendo delle precondizioni (condizioni sui parametri sotto le quali la specifica è definita e valida) e delle postcondizioni (effetti garantiti al termine dell’esecuzione dell’astrazione).

Programmazione per contratto

La presenta di pre e post condizioni introduce il tema della programmazione per contratto, dove possono variare solamente le proprietà non funzionali, che non sono vincolate da esso.

Le specifiche devono essere:

  • Generali: utilizzabili anche al di fuori del progetto specifico.
  • Minimali: slegate il più possibile dall’implementazione.
  • Robuste: il comportamento anomale deve essere previsto e gestito, e quindi la funzione definita deve essere totale.

I vincoli esprimibili da JML si categorizzano in:

  • modifiers
  • requires
  • assignable
  • ensures e result
  • signals

Modifiers

I modifiers sono delle etichette che descrivono le caratteristiche del metodo o delle variabili su cui si stanno imponendo i vincoli.

pure si impone su metodi, e indica che il metodo non ha side effects.

//@ pure
boolean isSorted(int[] a) { ... }

model si impone su una variabile, e permette di introdurre una variabile logica astratta che non esiste nel bytecode del programma. Questa non assume né valori né stati, e funge solo da etichetta.

//@ model int size;

ghost si impone su una variabile, e come model introduce una variabile non esistente nel Bytecode, tuttavia ha un valore e può cambiare durante il programma.

//@ ghost int counter;

Per assegnare alle variabili ghost si usa il modifier set.

//@ set counter = counter + 1;

Requires

requires impone delle precondizioni, e può essere omesso in caso una funzione sia totale.

//@ requires ...;

In caso la definizione di requires sia particolarmente complesso è opportuno ometterle e utilizzare signals.

Assignable

assignable segnala che un’entità è mutabile, e quindi può essere modificata durante la chiamata del metodo. Si applica a parametri dei metodi, variabili, oggetti e attributi degli oggetti.

//@ assignable nameVar;

È possibile specificare che nessuna variabile che rientra nel campo di visibilità di JML viene modificata:

//@ assignable \nothing:

Talvolta può essere utile usare il predicato \old.

Ensures e result

Indica le post condizioni tramite:

//@ ensures ...

Al suo interno si può usare il predicato \result che indica l’output, comparatori matematiche, formule aritmetiche complesse, metodi puri, oppure un insieme di valori indicati:

//@ ensures \result == [valore];

//@ ensures Math.abs(\result * \result) < 0.1;

Signals

I Signals permettono di verificare post-condizioni eccezionali lanciate in caso di violazione delle requires:

//@ signals (IllegalArgumentException e) x < 0;

Queste si specificano indicando il tipo di eccezione e la condizione logica che indica quanto verrà lanciata.

In caso esista solo un tipo di eccezione lanciabile dal metodo si può usare:

//@ signals_only (IllegalArgumentException e) x < 0;

È necessario che le condizioni delle Signals e Ensures siano ortogonali tra loro.

Altre clasusole e commenti

Esistono dei predicati in JML, oltre a quelli visti, che non rientrano in alcuna categoria, questi sono:

  • a ==> b: a implica b.
  • a <== b: b implica a.
  • a <==> b: a se e solo se b.
  • a <=!=> b: not a se e solo se b.
  • \old(E): valore di E precedente all’esecuzione del codice.
  • (* ... *): commenti testuali, da usare se i vincoli sono estremamente difficili da esprimere.

Quantificatori

JML supporta diversi tipi di quantificatori, tra cui:

  • Universale (\forall) ed Esistenziale (\exists).
  • Funzioni quantificatrici (\sum, \product, \min, \max).
  • Quantificatore numerico (\num_of).

In JML questi hanno una forma a tre campi:

(\forall Tipo v; range; condizione)

Dove il primo campo indica il tipo e il nome della variabile su cui predichiamo, il secondo campo indica il dominio ristretto in cui JML deve operare, e l’ultimo campo è il predicato che deve essere soddisfatto da ogni elemento del range.

Nelle funzioni quantificatrici e quantificatore numerico l’ultimo campo agisce come filtro che determina quali valori contare.

Astrazioni sui dati

Note

Con JML è possibile descrivere un nuovo tipo di dato astratto indicando valori e operazioni possibili. In questo modo, astraendo dai dettagli di rappresentazione dei valori e d’implementazione delle operazioni, il resto del programma dipende solo dalla specifica del tipo.

Siccome nelle classi i metodi possono agire sulle variabili di stato, non basta quanto visto per le astrazioni procedurali.

Si nota che i metodi pubblici puri (che non introducono side effects) sono indicati con /*@ pure @*/.

Example

Un esempio di metodo puro è size, che restituisce il numero di elementi di un contenitore, mentre un esempio di metodo non puro è insert.

public int /*@ pure @*/ size() { ... }

//@ ensures size()==\old(size())+1
public void insert(...) { ... }

Mutabilità

Un dato si dice mutabile quando ha metodi modificatori, cioè ha dei metodi che modificano lo stato dell’oggetto su cui vengono chiamati.

Specifica spec_public

La specifica spec_public permette di utilizzare un oggetto astratto tipico (OAT), che è un’implementazione astratta, generalmente la più semplice possibile.

//@ spec_public List<T> oat;

//@ ensures \result == aot.size();
public /*@ pure @*/ int size() { ... }

Proprietà astratte

Le proprietà astratte predicano su cose che sono valide per tutti gli oggetti in generale, ne esistono due tipi:

  • Proprietà invarianti: proprietà degli strati astratti invarianti.
  • Proprietà evolutive: proprietà sulla relazione tra uno stato e quello successivo.