- 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)))