----boundary-LibPST-iamunique-225550213_-_-
Content-type: text/plain
I don't see the problem. Neither the existing assignment of NIL to
'script', nor the one you suggest should be added, are actually
necessary to satisfy the post-condition. As 'script' is a pointer and
declared as an OUT parameter, BlackBox automatically initialises it to
NIL.
Chris Burrows
CFB Software
http://www.cfbsoftware.com/gpcp
> -----Original Message-----
> From: blackbox{([at]})nowhere.xy> Behalf Of Fyodor Tkachov
> Sent: Thursday, 3 March 2005 5:13 AM
> To: BlackBox Mailing List
> Subject: [BlackBox] - v.1.5 beta, Models, a bug
>
>
>
> An assingment is missing in the module Models of BlackBox v.1.5 BETA:
>
> PROCEDURE BeginScript* (m: Model; name: Stores.OpName;
> OUT script: Stores.Operation);
> (** post: (script # NIL) iff (m.domain # NIL) **)
> VAR seq: ANYPTR;
> BEGIN
> ASSERT(m # NIL, 20);
> IF m.Domain() # NIL THEN seq :=
> m.Domain().GetSequencer() ELSE seq := NIL END;
> IF seq # NIL THEN
> WITH seq: Sequencers.Sequencer DO
> seq.BeginScript(name, script)
> ELSE
> script := NIL (* this is
> missing **********************************)
> END
> ELSE script := NIL
> END
> END BeginScript;
>
--- BlackBox
--- send subject HELP or UNSUBSCRIBE to blackbox{([at]})nowhere.xy
----boundary-LibPST-iamunique-225550213_-_-
Content-type: application/rtf
Content-transfer-encoding: base64
Content-Disposition: attachment; filename="rtf-body.rtf"
e1xydGYxXGFuc2lcYW5zaWNwZzEyNTJcZnJvbXRleHQgXGRlZmYwe1xmb250dGJsDQp7XGYwXGZz
d2lzcyBBcmlhbDt9DQp7XGYxXGZtb2Rlcm4gQ291cmllciBOZXc7fQ0Ke1xmMlxmbmlsXGZjaGFy
c2V0MiBTeW1ib2w7fQ0Ke1xmM1xmbW9kZXJuXGZjaGFyc2V0MCBDb3VyaWVyIE5ldzt9fQ0Ke1xj
b2xvcnRibFxyZWQwXGdyZWVuMFxibHVlMDtccmVkMFxncmVlbjBcYmx1ZTI1NTt9DQpcdWMxXHBh
cmRccGxhaW5cZGVmdGFiMzYwIFxmMFxmczIwIEkgZG9uJ3Qgc2VlIHRoZSBwcm9ibGVtLiBOZWl0
aGVyIHRoZSBleGlzdGluZyBhc3NpZ25tZW50IG9mIE5JTCB0b1xwYXINCidzY3JpcHQnLCBub3Ig
dGhlIG9uZSB5b3Ugc3VnZ2VzdCBzaG91bGQgYmUgYWRkZWQsIGFyZSBhY3R1YWxseVxwYXINCm5l
Y2Vzc2FyeSB0byBzYXRpc2Z5IHRoZSBwb3N0LWNvbmRpdGlvbi4gQXMgJ3NjcmlwdCcgaXMgYSBw
b2ludGVyIGFuZFxwYXINCmRlY2xhcmVkIGFzIGFuIE9VVCBwYXJhbWV0ZXIsIEJsYWNrQm94IGF1
dG9tYXRpY2FsbHkgaW5pdGlhbGlzZXMgaXQgdG9ccGFyDQpOSUwuXHBhcg0KXHBhcg0KQ2hyaXMg
QnVycm93c1xwYXINCkNGQiBTb2Z0d2FyZVxwYXINCmh0dHA6Ly93d3cuY2Zic29mdHdhcmUuY29t
L2dwY3BccGFyDQpccGFyDQo+IC0tLS0tT3JpZ2luYWwgTWVzc2FnZS0tLS0tXHBhcg0KPiBGcm9t
OiBibGFja2JveEBvYmVyb24uY2ggW21haWx0bzpibGFja2JveEBvYmVyb24uY2hdIE9uXHBhcg0K
PiBCZWhhbGYgT2YgRnlvZG9yIFRrYWNob3ZccGFyDQo+IFNlbnQ6IFRodXJzZGF5LCAzIE1hcmNo
IDIwMDUgNToxMyBBTVxwYXINCj4gVG86IEJsYWNrQm94IE1haWxpbmcgTGlzdFxwYXINCj4gU3Vi
amVjdDogW0JsYWNrQm94XSAtIHYuMS41IGJldGEsIE1vZGVscywgYSBidWdccGFyDQo+IFxwYXIN
Cj4gXHBhcg0KPiBccGFyDQo+IEFuIGFzc2luZ21lbnQgaXMgbWlzc2luZyBpbiB0aGUgbW9kdWxl
IE1vZGVscyBvZiBCbGFja0JveCB2LjEuNSBCRVRBOlxwYXINCj4gXHBhcg0KPiBcdGFiIFBST0NF
RFVSRSBCZWdpblNjcmlwdCogKG06IE1vZGVsOyBuYW1lOiBTdG9yZXMuT3BOYW1lO1xwYXINCj4g
T1VUIHNjcmlwdDogU3RvcmVzLk9wZXJhdGlvbik7XHBhcg0KPiBcdGFiICgqKiBwb3N0OiAoc2Ny
aXB0ICMgTklMKSBpZmYgKG0uZG9tYWluICMgTklMKSAqKilccGFyDQo+IFx0YWIgXHRhYiBWQVIg
c2VxOiBBTllQVFI7XHBhcg0KPiBcdGFiIEJFR0lOXHBhcg0KPiBcdGFiIFx0YWIgQVNTRVJUKG0g
IyBOSUwsIDIwKTtccGFyDQo+IFx0YWIgXHRhYiBJRiBtLkRvbWFpbigpICMgTklMIFRIRU4gc2Vx
IDo9IFxwYXINCj4gbS5Eb21haW4oKS5HZXRTZXF1ZW5jZXIoKSBFTFNFIHNlcSA6PSBOSUwgRU5E
O1xwYXINCj4gXHRhYiBcdGFiIElGIHNlcSAjIE5JTCBUSEVOXHBhcg0KPiBcdGFiIFx0YWIgXHRh
YiBXSVRIIHNlcTogU2VxdWVuY2Vycy5TZXF1ZW5jZXIgRE9ccGFyDQo+IFx0YWIgXHRhYiBcdGFi
IFx0YWIgc2VxLkJlZ2luU2NyaXB0KG5hbWUsIHNjcmlwdClccGFyDQo+IFx0YWIgXHRhYiBcdGFi
IEVMU0VccGFyDQo+IFx0YWIgXHRhYiBcdGFiIFx0YWIgc2NyaXB0IDo9IE5JTCAoKiB0aGlzIGlz
IFxwYXINCj4gbWlzc2luZyAqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKioqKVxwYXIN
Cj4gXHRhYiBcdGFiIFx0YWIgRU5EXHBhcg0KPiBcdGFiIFx0YWIgRUxTRSBzY3JpcHQgOj0gTklM
XHBhcg0KPiBcdGFiIFx0YWIgRU5EXHBhcg0KPiBcdGFiIEVORCBCZWdpblNjcmlwdDtccGFyDQo+
IFxwYXINClxwYXINCi0tLSBCbGFja0JveFxwYXINCi0tLSBzZW5kIHN1YmplY3QgSEVMUCBvciBV
TlNVQlNDUklCRSB0byBibGFja2JveEBvYmVyb24uY2h9fQAAWJRSAAIBAAA/
----boundary-LibPST-iamunique-225550213_-_---
Received on Thu Mar 03 2005 - 00:11:25 UTC