Volevo sapere in jml, la num of, come funzione, quando va fatta e alcuni esempi, mi potete aiutare?
Volevo sapere in jml, la num of, come funzione, quando va fatta e alcuni esempi, mi potete aiutare?
La sintassi della num_of in JML è la stessa della forall:
//@ (\num_of TIPO var; Condizione1(var); Condizione2(var))
Quindi la num_of "restituisce" il numero totale di volte che viene verificata la:
Condizione1(var) e CONTEMPORANEAMENTE la Condizione2(var)...
Se ad esempio devi contare quante volte compare il numero 5 in un array
//@ (\num_of int i; i>=0 && i<array.length; array[i] == 5)
Ciao.
...c'è chi come te attende l'alba...
grazie, chiarito!!!
Permessi di invio
Rispondi quotando