- ral-from-upto ls from uptoprocedure
-
function (result) requires (and (ral? ls) (fixnum? from) (fixnum? upto) (fx>= from 0) (fx>= upto from) (fx<= upto (ral-count ls))) ensures (and (ral? result) (fx= (ral-count result) (fx- upto from)))
function (result) requires (and (ral? ls) (fixnum? from) (fixnum? upto) (fx>= from 0) (fx>= upto from) (fx<= upto (ral-count ls))) ensures (and (ral? result) (fx= (ral-count result) (fx- upto from)))