Obfuscated Abstract Data Type

Abstract data type O over items of type int has the following interface (here written as Java code):

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
public class O {

/** Constructor: precondition true; postcondition Q() */
public O() { ... }

/** Query: precondition true */
public boolean Q() { ... }

/** Query: precondition ! Q() */
public int S() { ... }

/** Command: precondition true; postcondition ! Q() */
public P(int i) { ... }

/** Command: precondition ! Q() */
public R() { ... }

}

It satisfies the following four properties for every instance O o and item int i.

  1. If o.Q() holds, then o.P(i) establishes o.S() == i .
  2. If ! o.Q() holds, then o.P(i) preserves o.S() (that is, o.S() is invariant/unchanged).
  3. If o.Q() holds, then o.P(i); o.R() preserves o.Q().
  4. If ! o.Q() holds, then o.P(i); o.R() and o.R(); o.P(i) are equivalent.

What abstract data type is O?

Notes:

  • ! means "not" (boolean negation)
×

Problem Loading...

Note Loading...

Set Loading...