Lab06Ejercicio1.gcl

[
const​ S: array[0..N) of int;

{ N > 1 }

mostrar(orden(S))

func orden( S: array [0..N) of int ) → B array [0..2) of bool
{Pre: N > 0 }
{Post: (% forall i: int | 0 <= i /\ i < N-1 | S[i]>S[i+1] \/ creciente=True) \/
              (% forall i: int | 0 <= i /\ i < N-1 | S[i]<=S[i+1] \/ decreciente=True) \/
                       ((desordenado!=creciente) \/ (desordenado=True))
 }
[
    var S : array [0..N) of int;
    var B : array [0..2) of int;
    var i : int;
    var creciente : bool;
    var decreciente : bool;
    var desordenado : bool;
    i := 0;
    creciente := False;
    decreciente := False;
    desordenado := False;
    do i<N-1 and desordenado==False →
        if S[i]<=S[i+1] →
            creciente := True
            if decreciente==True /\ creciente==True →
                desordenado := True
        [] S[i]>S[i+1] →
            decreciente := True
            if decreciente==True /\ creciente==True →
                desordenado := True
        fi
        i := i+1
    od;
    B[0]:= creciente;
    B[1]:= decreciente;
    B[2]:= desordenado;

    >> B
]

func mostrar( B : array [0..2) of bool ) -> int:
{Pre: True }
{Post: (B[2]=True /\ o=0) \/ (B[1]=True /\ o=-1) \/ (B[0]=True /\ o=1)}
[
    var o : int;

	if B[2]==True:
		o := 0
    [] B[2]==False:
        skip 
	[] B[1]==True:
		o := -1
    [] B[1]==False:
        skip
	[] B[0]==True:
		o := 1
    [] B[0]==True:
        skip    
    >> o
]

{True}