[MUD-Dev] Object Models

[John Buehler]

Phillip Lenhardt writes:

> Suppose you have a component called Sorter that takes an array of
> Integers and a pointer/reference (or whatever your language supports)
> to another component called Comparer and returns a "sorted" array
> of Integers. Comparer takes two Integers as arguments and returns
> a Boolean: True if the first Integer argument is greater than or
> equal to the second Integer argument and False otherwise.
>
> So the contract as I've stated it above guarantees that the right types
> get passed in and the right types get returned. But how do you specify
> in the contract that whatever algorithm Sorter uses actually returns
> an Integer array such that if you passed the Nth and Nth + 1 elements
> of the array to Comparer, the Comparer will return True (ie the array
> is sorted in descending order)? You can't just analyze the algorithm
> used by Sorter because that could very well be a non-terminating or
> _very_ long process. I suppose you _could_ have a post-condition of the
> contract actually do the comparison of the Nth and Nth + 1 elements for
> every pair of elements in the array, but that's horribly inefficient.

We went the horribly-inefficient route.  We would supply sample data sets to
the component's method and then verify the results.  This was done until all
blocks and arcs were covered, as well as whatever testing was necessary to
cover discrete test cases.  That is, we obviously didn't give it every case
in the spectrum of 'all possible integer arrays', but we gave it enough to
ensure that no matter what the component did inside, it resulted in a
properly-sorted array.  Which is not a guarantee that there were no arrays
of integers that could be returned improperly sorted.  But if the set of
arrays that WERE supplied were reasonably representative (that is,
non-trivial), then we end up with high confidence that the type of the
component is properly established.

This process happened in isolation, before the component was deployed, in
order to establish the type of the component.  That 'type' includes the
statement that the component does the sorting as you've described.

> There's a whole class of languages--Haskell, SML, Clean, etc--that
> treat programs as a series of functions calling other functions. That's
> "function" in the mathematical sense: the exact same input _always_
> results in the exact same output; not just type-sameness, but value-
> sameness. And none of those languages try to make sweeping guarantees
> that the results you get will be the ones you want, just that you will
> get the _same_ results every time you provide the same input. And
> components can't make that weaker guarantee, even though you claim
> they can enforce even stronger guarantees.

My apologies if I've overstated the possibilities with components.  Such was
never my intent.

Also, I'm starting to get nervous about talking about this stuff in detail -
for legal reasons.  I've talked about the depth that I have because I've
seen public comments by Clemens along these lines, but I'm not sure where
the final line is drawn.

JB


_______________________________________________
MUD-Dev mailing list
MUD-Dev at kanga.nu
https://www.kanga.nu/lists/listinfo/mud-dev