1
$\begingroup$

I have created a very basic model of an array list in the B method as shown below

MACHINE Array(TYPE)

VARIABLES block

INVARIANT block : seq(TYPE)

INITIALISATION block := []

OPERATIONS

add(e) =
   PRE e : TYPE
   THEN block := block <- e
   END;

remove =
   PRE block /= []
   THEN block := tail(block)
   END;

res <-- showArray =
    res := block;

res <-- getfront =
   PRE block /= []
   THEN res := first(block)
   END

END

However what I am trying to achieve is to create a model that prevents deletion from the list, so when an element is added, it cannot be deleted.

What should I add in the invariant to achieve this?

$\endgroup$
1
$\begingroup$

You cannot add such a property to your invariant because the invariant describes how a valid state might look like but not how it can be altered.

The operations are responsible for specifying the behaviour of the model. If you want to prevent that an element will be removed from the array, just do not specify that as a possible behaviour. In your example above, just remove the operation remove.

Every valid refinement is then not allowed to remove an element.

$\endgroup$
0
$\begingroup$

Add a postcondition to each operation stating that if the array held an element before the operation, then the element is still present afterwards. In other words, if $A[i]=x$ held before the operation, then $A[i]=x$ still holds. I'll let you work out how to express this in formal mathematics and prove by induction that this achieves what you want, since this is your exercise.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.