CompresionMensaje.gcl

[Ctx C: mens[0..n-1]:char
    {Pre Q: mens[////////////////////]}

    k:= 0;
    mc := [0..n-1];
    j:= 0;
    ea := T

    {Inv P: mc [/////          ] & k>= 0}

    {Cota t: n - k + 1}

    do k != n-1 ->
        if mens[k] != '-' ->
            mc[j] := mens[k];
            j:= j + 1;
            ea := T
        [] mens[k] == '-' & ea = T ->
            mc[j] := '-'
            j := j + 1;
            ea := False
        fi

        k := k + 1;
    od

    {Pos R: mc [////////////////////            ]}
]