Re: Criteria to decide what is private? [LONG]

Daniel T. wrote:

In article <eoq7nm$o8t$1@xxxxxxxx>, S Perryman <q@xxxxx> wrote:

The invariant is *already exposed* to "outsiders" , merely by being *defined* in the type spec. What has the addition of set ops done to
change this ??

(I define outsiders here as the users/inheritors of the Range type - if
this is not what you intend the term to mean, feel free to provide your
definition and we can re-discuss)

Our definitions of "outsiders" is the same, but I meant something different by the word "exposed". I meant that the invariant can be broken by outsiders.

OK. So this by definition means that an outsider can only break a type
invariant when accessing a type property P, by not conforming to the
pre-conditions defined for P (preconditions(P) ) .


If we put sets in the class with conventional definitions

What is the "conventional definition" ??

void setLow( int v ) {
low = v;
}

This is a typical implementation.
I wanted a typical specification (pre/post-conditions) .


DT>If you add "setLow( int L )" to the interface above, what will be its
DT>postcondition?

We have :

pre-conditions(setLow) = {}
post-conditions(setLow) = {}
invariant(Range) = low() <= high()

This is a viable option. It says that setLow does not do anything at all. As such an implementation that does nothing for any value of L is completely correct.

Oh no. It says no such thing.
The post-condition (correctly) states that whatever value low/high are
set to as a result of being given L, low <= high.


So:

pre(setLow) = post(setLow) = (low() <= high() )

I have a Range instance R, that currently represents the range [2,3] .
I do the following :

R.setLow(4) ;

What happens with the correctness artifacts ??

- pre(setLow) = true.

obviously

- post(setLow) = true.

obviously

What are the subsequent values of high/low after invoking setLow ??

UNDEFINED !!!

That is not how I understand contracts. As I understand it, there is an implied contract that any state not mentioned in the postcondition will remain invariant.

1. Sadly not. In the words of Liskov and Wing :

Type Specifications Need Explicit Invariants
Type Specifications Need Explicit Constraints


Assume nothing. Specify as much as possible.


2. Here is an exercise that examines the notion of other "state not
mentioned in the postcondition" remaining invariant. It is the old
favourite of type substitutability ... Circle/Ellipse.

type Ellipse
do
invariant : focusA() > 0 , focusB() > 0

pre: A > 0
post: focusA() = A
setFocusA(A) ;

pre: B > 0
post: focusB() = B
setFocusB(B) ;
end


type Circle
conforms to Ellipse
do
invariant: radius() = focusA() = focusB()

setFocusA(A) ;
setFocusB(B) ;
end


Circle c = new Circle(radius : 1) ;

c.setFocusA(2) ; // #1
c.setFocusB(3) ; // #2


Q1. What are the contracts for Ellipse::focusA(A) etc as actually
written ?? What are they for Circle::focusA(A) ??

Based on these contracts, what will the values of c.focusA() and
c.focusB() at points #1/#2 ??

Do those values conform to the contracts of Ellipse/Circle::focusA(A) ??


Q2. Repeat Q1, but replace "contracts" with "implied contracts" and
"as actually" with "when explicitly" .

Q3. Is there a difference between Q1 and Q2 ?? If so, what is the
difference ?? If there is a difference, how easy is it for a user of
a type to discern such implied contracts ??


The Range type has *no statement* of what those values will be.
All we know is whatever the values are, low <= high.

If you make it: low() == L

Now we have :

pre(setLow) = low() <= high()
post(setLow) = (low() == L) AND (low() <= high() )

I have a Range instance R, that currently represents the range [2,3] .
I do the following :

R.setLow(4) ;

What happens with the correctness artifacts ??

- pre(setLow) = true.

obviously

- post(setLow) = true.

obviously

What are the subsequent values of high/low after invoking setLow ??

low = 4
high = UNDEFINED !!!

The Range type has *no statement* of what the high value will be.
All we know is whatever the values are, low <= high.

Again, this may be a misunderstanding on my part. If it is, then you are correct, of course.

It may or may not be a misunderstanding (that remains to be shown) .

If it isn't, we need to state your understanding precisely so that we can
discuss things further.

If it is, we still need to state your understanding precisely, so that we
can see which parts of your understanding are correct, and which are not.

Either way, we are going to get there.


Regards,
Steven Perryman
.