Re: [xml-dev] Notable declarative expressions?

[Dimitre Novatchev <dnovatchev@gmail.com>]

Hi Roger,

> Answer to Problem #2

> Here is a declarative description of the change in the pile:

>          The pile after is equal to the pile before,
>          minus one item.

> Here is how the constraint is expressed using the Alloy language:

>        before, after: Time | pile.after = pile.before - item


I think this answer is not entirely correct. What also must be
verified is that nothing else in the surrounding universe got
modified.

There is a clear analogy with testing a program -- we want to verify
that it did what it was expected to do, **and nothing else**  -- for
example it didn't put binary zeroes in the rest of the RAM allocated
to this program.

Cheers,
Dimitre


On Sun, Dec 18, 2016 at 10:19 AM, Costello, Roger L. <costello@mitre.org> wrote:
>
> Hi Folks,
>
> Do you have a notable declarative expression that you can share?
>
> An XML Schema is a model; specifically, a data model. When you create an XML Schema, you are “data modeling.”
>
> A key skill for modeling (both data modeling and software modeling) is the ability to think and express declaratively.
>
> Below are two problems and their declarative expressions.
>
> Problem #1
>
> Declaratively express this constraint:
>
> A set of nodes must form ring (cyclic) topology.
>
> The following graphic shows a set of nodes with a ring topology:
>
> Assume each node has a succ field, identifying its neighbor. How would you declaratively constrain the nodes to a ring topology?
>
> Scroll down to see the answer …
>
> Problem #2
>
> Declaratively express the change in this pile of items:
>
> Scroll down to see the answer …
>
> …
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
>
> Answer to Problem #1
>
> Here is a declarative description of constraining nodes to form a ring topology:
>
> All nodes must be reachable from any node
> by following succ repeatedly.
>
> Here is how the constraint is expressed in the modeling language called Alloy:
>
> all n: Node | Node in n.^succ
>
> For each Node n, the entire set of nodes must be in the set of nodes reachable by n.
>
> The caret symbol denotes the set of nodes reachable from n.
>
> Give a set of nodes, plus the above constraint expression, to a constraint satisfaction (SAT) tool and the SAT tool will decide if the nodes satisfy the constraint (i.e., the SAT tool will tell you if the nodes are in a ring structure).
>
> Answer to Problem #2
>
> Here is a declarative description of the change in the pile:
>
> The pile after is equal to the pile before,
> minus one item.
>
> Here is how the constraint is expressed using the Alloy language:
>
> before, after: Time | pile.after = pile.before - item
>
> Important: That expression is not a recipe/algorithm/procedure for how to remove an item from the pile. Rather, it is a description of the pile after by comparing it to the pile before.
>
> /Roger




-- 
Cheers,
Dimitre Novatchev
---------------------------------------
Truly great madness cannot be achieved without significant intelligence.
---------------------------------------
To invent, you need a good imagination and a pile of junk
-------------------------------------
Never fight an inanimate object
-------------------------------------
To avoid situations in which you might make mistakes may be the
biggest mistake of all
------------------------------------
Quality means doing it right when no one is looking.
-------------------------------------
You've achieved success in your field when you don't know whether what
you're doing is work or play
-------------------------------------
To achieve the impossible dream, try going to sleep.
-------------------------------------
Facts do not cease to exist because they are ignored.
-------------------------------------
Typing monkeys will write all Shakespeare's works in 200yrs.Will they
write all patents, too? :)
-------------------------------------
Sanity is madness put to good use.
-------------------------------------
I finally figured out the only reason to be alive is to enjoy it.