Date: Thu, 22 Feb 2007 20:21:17 +0000
From: Nuno Correia

Hi there. This is first contribution to this list... I'm sorry that it's to
ask you for help rather than to actually contribute.

I'm having some trouble understanding why this predicate:

------

pred OpenAccount(b, b': BAMS, id: AccId, hldr: set AccHolder, amt: Int) {
    id not in (b.bams).univ
    b'.bams.h = b.bams.h + id->hldr->amt
}

------

given these signatures:

------

sig BAMS { bams: AccId lone-> Account }

sig Account { h: set AccHolder -> Int }

sig AccId, AccHolder {}

------

doesn't give me a different value for OpenAccount_b', as it's basically
identical to the add predicate from section 2.2 of Software Abstractions.

Also, should I be doing this this way at all? This is a more or less literal
translation from an existing VDM specification where OpenAccount was a
function which performed a map union between the corresponding BAMS type (a
mapping from AccId to Account) with the tuple to be added. I figured the
predicate would capture the notion of transformation well.

Thanks for the time,
Nuno Correia