**ParaSail**, some interesting things start to happen. Unless programmers are very familiar with writing pre- and postconditions as a matter of course, chances are that the code will be written initially with few if any pre/postconditions. However, presuming that the language-provided abstractions, such as Arrays, already have some preconditions (such as you cannot index into an array with an index that is out of the array bounds), the compiler pretty quickly identifies places where the programmer will

*have*to write some of their own preconditions, constraints, invariants, etc. For example, consider the classic Stack abstraction. This might be written in ParaSail as follows, initially without any pre/postconditions:

This all looks pretty straightforward until we try to compile it, and the compiler begins to complain at various places. For example, we blithely add one to S.Cur_Len in Push without any apparent concern about overflow. Then we blithely use the incremented S.Cur_Len as an index into S.Data, again with no apparent concern for the index being out of bounds.interfaceStack <ComponentisAssignable<>; Size_TypeisInteger<>>isfunctionCreate(Max : Size_Type) -> Stack;functionTop(S :refStack) ->refComponent;procedurePop(S :refvarStack);procedurePush (S :refvarStack; X : Component);endinterfaceStack;classStackisconstMax_Len : Size_Type;varCur_Len : Size_Type;typeIndex_TypeisSize_Type{Index_Type in 1..Max_Len};varData : Array<optionalComponent, Indexed_By => Index_Type>;exportsfunctionCreate(Max : Size_Type) -> Stackisreturn(Max_Len => Max, Cur_Len => 0, Data => [.. =>null]);endfunctionCreate;procedurePush(S :refvarStack; X : Component)isS.Cur_Len += 1; S.Data[S.Cur_Len] := X;endprocedurePush;functionTop(S :refStack) ->refComponentisreturnS.Data[S.Cur_Len];endfunctionTop;procedurePop(S :refvarStack)isS.Cur_Len -= 1;endprocedurePop;endclassStack;

The ParaSail compiler is never

*blithe*, and will complain because the Array abstraction imposes a precondition on the indexing into S.Data, requiring that the index be in the range of Index_Type (1..Max_Len). It will also complain because the increment of S.Cur_Len might cause it to exceed the maximum Size_Type value (this precondition is from the "+=" operation of the Integer abstraction).

We could resolve these problems by adding a meaningful constraint on the range of values of Cur_Len (namely

*{Cur_Len in 0 .. Max_Len}*) and adding a precondition on the Push operation ensuring that Cur_Len < Max_Len before any call on Push. However, Cur_Len and Max_Len are not exported in the Stack interface, so we need to provide functions that reveal their value, say "Count" and "Max_Stack_Size." So our new Stack abstraction would look like this:

So with these changes, Push should now compile. However, we are going to run into similar problems in Top and Pop, and we will need a precondition on both of those ofinterfaceStack <ComponentisAssignable<>; Size_TypeisInteger<>>isfunctionMax_Stack_Size(S : Stack) -> Size_Type;functionCount(S : Stack) -> Size_Type;functionCreate(Max : Size_Type) -> Stack;functionTop(S :refStack) ->refComponent;procedurePop(S :refvarStack);procedurePush (S :refvarStack{Count(S) < Max_Stack_Size(S)}; X : Component);endinterfaceStack;classStackisconstMax_Len : Size_Type;varCur_Len : Size_Type{Cur_Len in 0..Max_Len};typeIndex_TypeisSize_Type{Index_Type in 1..Max_Len};varData : Array<optionalComponent, Indexed_By => Index_Type>;exportsfunctionMax_Stack_Size(S : Stack) -> Size_TypeisreturnS.Max_Len;endfunctionMax_Stack_Size;functionCount(S : Stack) -> Size_TypeisreturnS.Cur_Len;endfunctionCount;functionCreate(Max : Size_Type{Max > 0}) -> Stackisreturn(Max_Len => Max, Cur_Len => 0, Data => [.. =>null]);endfunctionCreate;procedurePush (S :refvarStack{Count(S) < Max_Stack_Size(S)}; X : Component)isS.Cur_Len += 1; S.Data[S.Cur_Len] := X;endprocedurePush;functionTop(S :refStack) ->refComponentisreturnS.Data[S.Cur_Len];endfunctionTop;procedurePop(S :refvarStack)isS.Cur_Len -= 1;endprocedurePop;endclassStack;

*{Count(S) > 0}*. Top also presents a more subtle problem. The Data array is defined as being an array of

**optional**Element_Type, but we are returning S.Data[S.Cur_Len] with a return type of simply Element_Type, implying that we somehow know that S.Data[S.Cur_Len] is not

**null**. So how do we know that? Well, we know that Push only pushes non-null elements onto the stack (because the parameter type for X is a non-

**optional**Element_Type. But Data starts out all null, and when looking only at Top we have no way of knowing that S.Data[S.Cur_Len] is not null.

What we need is some kind of class

*invariant*which ensures that when we get into Top, S.Data[S.Cur_Len] is not null. What might that invariant look like? What we know about a stack is that all of the elements that have been pushed onto the stack are non-null, but the slots in the stack past Cur_Len might be null if they have never been used. So our invariant would seem to be:

The basic requirement for a class invariant is that, presuming it is true on entering any externally visible operation, it is true again on exiting that operation. It might be false in the middle of some operation, but it is{for all I in 1..Cur_Len => Data[I] not null}

*preserved*overall by all visible operations. Furthermore, for any operation that creates an object of type Stack, the returned object must satisfy the invariant.

So let us check whether the above proposed invariant is true upon creation of a Stack object, and is preserved by operations that modify a Stack. Create produces a new value with Cur_Len == 0, so the invariant is trivially true, since there are no values in the interval 1..Cur_Len. Push and Pop modify a Stack object. Pop is trivial since it is decrementing Cur_Len, so the interval 1..Cur_Len is shrinking. Push is not trivial, because it is adding one to Cur_Len. But if we presume the invariant holds on entry to Push, then the only new value to worry about is S'.Data[S'.Cur_Len], where S' represents the value of S after the Push operation is complete. Since S'.Data[S'.Cur_Len] is set to X, and X is not null, our invariant is preserved.

Note that we might have tried an invariant of simply

*{Data[Cur_Len] not null}*, which would have satisfied Top, and would be preserved by Push, but it would not be preserved by Pop, since without the more sophisticated invariant, Pop would know nothing about S'.Data[S'.Cur_Len]. It might be null if the invariant only claims that the very top element is non-null.

So after adding the class invariant, and the various preconditions, we can now get the Stack abstraction to compile. However, it now becomes time to write some code that tests the Stack abstraction. What we quickly discover is that the compiler rejects any call on any Stack operation with a precondition, since there are no postconditions that would allow it to know whether Count(S) > 0 or Count(S) < Max_Stack_Size(S). At the call site there is no

*peeking*into the

**class**that defines the

**interface**. The compiler must prove the preconditions of the call looking only at information in the

**interface**. And without any postconditions, the compiler is stuck.

So now we have to start adding postconditions to the operations. If we do a Create and then immediately try to do a Push onto the created stack object, our first job is to prove that Count(S) < Max_Stack_Size(S). This implies we need a postcondition on Create that indicates the values of Count() and Max_Stack_Size() for the result of Create. We could write this as follows:

What this says is that the result of Create (within a postcondition, we can use the name of the creating function to represent the result) has a Max_Stack_Size that corresponds to the passed in parameter Max, and starts out with a Count of zero. No big surprise here, but without such a postcondition the compiler would be pretty much at a loss. We also might want to impose a precondition on Max of{Max_Stack_Size(Create) == Max; Count(Create) == 0}

*{Max > 0}*just so the stack is at least of some use.

Next question we might have is what happens to Count as a result of Push. This brings up an interesting question that is sometimes called the

*frame*problem. How do we know what might be written by an operation -- what is the

*write frame*? (We might also be interested in exactly what might be read by an operation -- what is the

*read frame*-- but that is less relevant as far as checking preconditions.) Since the Push operation has S as a

**ref var**parameter, we could assume the worst and assume any function of S' (the value of S after Push) might return a different value, so after Push we know pretty much nothing about Count(S') and Max_Stack_Size(S'). Alternatively, we could take the view that if there is no postcondition, then nothing is changed.

For ParaSail we are (tentatively) adopting a model that for any function of S mentioned in any precondition of an operation on a Stack object S, if such a function is not mentioned in a postcondition then it is presumed unchanged. Now that we have mentioned Count() and Max_Stack_Size() in the preconditions of Push, we are duty bound to write postconditions any time the value of Count() or Max_Stack_Size() is changed. This obligation will be checked when we compile the Stack class, so having written some preconditions, the compiler is going to start complaining because Count(S') is clearly going to be different from Count(S) after the call on Push. Similar obligations will apply to Pop. So now we will need to add a postcondition to Push of

*{Count(S') == Count(S) + 1}*and a postcondition to Pop of

*{Count(S') == Count(S) - 1}*. We don't need to say that

*{Max_Stack_Size(S') == Max_Stack_Size(S)}*because as indicated, our default assumption is that anything used in any precondition, but not mentioned in a postcondition, is presumed to be unchanged by the operation. Again, the compiler will check that when it compiles the code for the operation. If we don't want to say anything about the new value other than it is not the same as the old value, we could say {Some_Property(S') != Some_Property(S)}. That won't help the compiler with proving later preconditions, but it will at least satisfy the obligation to mention the changed property in a postcondition.

So if we continue this process until we make the compiler happy, both with the Stack module itself, and with our various test programs, we will probably end up with a relatively fully annotated Stack like the following:

One thing to note is that the compiler has not forced us to create postconditions that ensure all the nice properties of Stacks, such as after Push(S,X), then Top(S') == X, or if Top(S) == A, then after Push(S, X) and Pop(S'), Top(S'') == A. These might be calledinterfaceStack <ComponentisAssignable<>; Size_TypeisInteger<>>isfunctionMax_Stack_Size(S : Stack) -> Size_Type;functionCount(S : Stack) -> Size_Type;functionCreate(Max : Size_Type{Max > 0}) -> Stack{Max_Stack_Size(Create) == Max; Count(Create) == 0};procedurePush (S :refvarStack{Count(S) < Max_Stack_Size(S)}; X : Component){Count(S') == Count(S) + 1};functionTop(S :refStack{Count(S) > 0}) ->refComponent;procedurePop(S :refvarStack{Count(S) > 0}){Count(S') == Count(S) - 1};endinterfaceStack;classStackisconstMax_Len : Size_Type;varCur_Len : Size_Type{Cur_Len in 0..Max_Len};typeIndex_TypeisSize_Type{Index_Type in 1..Max_Len};varData : Array<optionalComponent, Indexed_By => Index_Type>;exports{forallIin1..Cur_Len => Data[I]notnull}// invariant for Top()functionMax_Stack_Size(S : Stack) -> Size_TypeisreturnS.Max_Len;endfunctionMax_Stack_Size;functionCount(S : Stack) -> Size_TypeisreturnS.Cur_Len;endfunctionCount;functionCreate(Max : Size_Type{Max > 0}) -> Stack{Max_Stack_Size(Create) == Max; Count(Create) == 0}isreturn(Max_Len => Max, Cur_Len => 0, Data => [.. =>null]);endfunctionCreate;procedurePush (S :refvarStack{Count(S) < Max_Stack_Size(S)}; X : Component){Count(S') == Count(S) + 1}isS.Cur_Len += 1; S.Data[S.Cur_Len] := X;endprocedurePush;functionTop(S :refStack{Count(S) > 0}) ->refComponentisreturnS.Data[S.Cur_Len];endfunctionTop;procedurePop(S :refvarStack{Count(S) > 0}){Count(S') == Count(S) - 1}isS.Cur_Len -= 1;endprocedurePop;endclassStack;

*correctness*preconditions as opposed to merely

*safety*preconditions, and they are up to the programmer to add if they see fit. We have considered having a

*second class*annotation in ParaSail which is

*not*required to be provable at compile-time, but is designed to aid in correctness proofs, and provide additional debugging support. We have set aside a syntax of doubly nested

*{{...}}*for such correctness preconditions, but we aren't worrying about them more than that at this point.

## No comments:

## Post a Comment