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