Programacio metodica

PROGRAMACIÓ METÒDICA.

Part 1.

Expert:

1. Donat el següent algorisme:

IDENTIFICADOR TIPUS

n,p,s,i enter

{ n=N  N  1 }

p 1

s  1

i  0

Mentre i<n fer

i  i + 1

p 2 p

s  s + p

Fi_mentre

{ Q }

I={ p=2i  s=k: 0ki:2k  i N }

(a) Quina és la fita de la iteració?

fita=N-i

(b) Trobeu la postcondició Q i expliqueu-la.

{I ^ ¬B}=>Q

Q={p=2^i ^ s=Ek:0<=k<=i:2^k ^ n=N ^ i<=N} ^ {i>=n}

(c) Verifiqueu formalment l’algorisme. El bucle acabarà?

PROGRAMACIÓ METÒDICA.

Membres del grup:

Part 2.

Expert:

2. Donat el següent algorisme:

IDENTIFICADOR TIPUS

n enter

sum enter

{ n=N  N  0 }

i  1

sum  1

f 1

Mentre in+1 fer

sum  sum+f

i i+1

f f*i

Fi_mentre

{ sum=k: 0kn: k! }

(a) Trobeu l’invariant i la fita de la iteració. Expliqueu-los.

(b) Comproveu formalment la correctesa de l’algorisme. Si l’algorisme no satisfà. l’especificació, doneu les modificacions que hi faríeu per assegurar la correctesa.

PROGRAMACIÓ METÒDICA.

Part 3.

Expert:

3. Donat el següent algorisme:

IDENTIFICADOR TIPUS

t taula(0..N-1) d’enters

{ n=N ^ N > 0 } {la taula està inicialitzada}

i  1

k 0

mentre i < n fer

si t(i)  t(k) llavors acció nul•la

t(i) > t(k) llavors k i

fi_si

i  i+1

fi_mentre

{ Q }

(a) Quin és l’invariant i la fita de la iteració?

(b) Quina és la postcondició de l’algorisme?

(c ) Verifiqueu formalment l’algorisme.

.

...