Express What, not How.

[David Eppstein]

In article <4u65ir2eya.fsf at vex.net>, Albert Lai <trebla at vex.net> wrote:

> It is a functional (immutable) abstract data type, so most operations
> take an existing instance as a parameter and return a new instance.
> The name of the abstract data type is LiDui.
> 
> Hung  : LiDui
> MoYun : LiDui -> Bool
> PaiDui: (LiDui,Object) -> LiDui
> DuiTau: LiDui -> Object
> LeiDui: LiDui -> LiDui
> 
> MoYun(Hung) is true.
> For any LiDui d:
>   If MoYun(d) is true, we have LeiDui(PaiDui(d,o))=d and 
>   DuiTau(PaiDui(d,o))=o.
>   If MoYun(d) is false, we have LeiDui(PaiDui(d,o))=PaiDui(LeiDui(d),o).
> 
> That's it.

You sure you don't need a little more?  This seems to fit both stacks 
(MoYun always = True) and queues (MoYun true only for Hung).

That's one trouble with axiomatic definitions -- it's hard to be sure 
you've expressed all of the behavior you intend to specify.
Another is that they can be difficult to understand.

-- 
David Eppstein                      http://www.ics.uci.edu/~eppstein/
Univ. of California, Irvine, School of Information & Computer Science