allow shape shape updates in bff
authorHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Feb 2014 15:15:03 +0000 (16:15 +0100)
committerHelmut Grohne <grohne@cs.uni-bonn.de>
Fri, 7 Feb 2014 15:15:03 +0000 (16:15 +0100)
Unlike the original version in VoigtlaenderHMW13, we do not request an
  sput : ℕ → ℕ → Maybe ℕ
function for determining the updated source shape from the original
source and updated view shape. Instead we ask the caller directly to
provide the result of sput together with a proof that its getlen matches
with the provided, updated view.

The precondition assoc-enough is not enriched in this way and still
requires a non-changing shape. I.e. it says what it said before.


No differences found