[Prev][Next][Index]

Re: A miscellany

David,

I agree that a "hidden" bag sort is fine way to define perm.

But for this to really specify perm properly, the operators on bags that
are used have to be pinned down pretty precisely.  I'd expect that
regardless of the model chosen, all the terms that are used in the
specification of perm are completely determined.  (If they aren't, perm
isn't guaranteed to test correctly for a permutation.)  So within
package integer_lists there isn't any difference between the E- and
A-interpretations.

I would expect that the unwary user of package P would find that it was
indeed safe to identify the notion of int_bags occurring in the
annotations of package P with that of int_bags occurring in int_list, as
long as he or she reasoned about them using only the (shared) axioms about
int_bags from IntegerCombinatorics.

I have the feeling that there is some basic assumption made by Larch/Ada
that I'm just overlooking, or some basic assumption in LM3 and LCL that
Larch/Ada doesn't share.  Could this be the case?

Jim H.