On Thu, 29 Mar 2018, Jean-Christophe Filliatre wrote:
> Hi Julia,
>
> > but at the call site of the function that contains this code, it complains
> > that:
> >
> > warning: this expression may diverge, which is not stated in the
> > specification
> >
> > Can I just ignore the warning?
>
> If you are not interested in proving termination, yes you can.
>
> > I would like the whyml code to look like what one would most naturally
> > write in an imperative language, so I didn't want to wriet a recursive
> > function.
>
> As far as termination is concerned, Why3 makes no difference between
> while loops and recursive functions. If ever one or the other is used
> without a termination argument (a variant), then the surrounding
> functions has "diverges" (potential non-termination) as part of its
> effects, and that non-termination effect propagates whereever the
> functions is called.
Based on an example I found in the manual, the current code is:
while !rdy <> Nil
do
variant { !rdy }
let t = head !rdy in
(if cores.cload[selected] - cores.cload[self] >= 2 * t.load
then
begin
... (* no modification to rdy *)
end);
rdy := tail !rdy;
done
Prior to this, I have:
let rdy = ref cores.ready[selected] in
and the ... does do eg:
cores.ready[selected] <- remove t cores.ready[selected]
Will that have an impact on rdy? I don't really know how mutable things
work.
thanks,
julia
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
