[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 [////////////////////            ]}