{"entities":{"Q911245":{"pageid":913093,"ns":120,"title":"Item:Q911245","lastrevid":49366546,"modified":"2026-01-07T01:12:11Z","type":"item","id":"Q911245","labels":{"en":{"language":"en","value":"Observational implementation of algebraic specifications"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4141467"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$52DB419A-D797-460E-A533-AD9062859820","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"2f90793ece9f7b8cbd633165b8b74705f5a5d03a","datavalue":{"value":{"text":"Observational implementation of algebraic specifications","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q911245$168A8481-C9A1-4A7A-9473-5D0B43D63299","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"7a7e6c960257dcfbe5c528ccac778bfddfe67276","datavalue":{"value":"0696.68026","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q911245$87F23566-2D8A-4D29-A726-396D3EC7E147","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"59e245c4cace4d400d6941555edf33c7aec4899a","datavalue":{"value":"10.1007/BF01178505","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q911245$54B96262-065D-4483-8723-655A4EBAE8A9","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"82d7e2ad3382677d83b89ec58edf18af8299f3c0","datavalue":{"value":{"entity-type":"item","numeric-id":549176,"id":"Q549176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$8161D917-DB6C-4161-9522-AE86FA54A7CC","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"7d0f02e85530cd06ceb2c58a40dc9c2e0258e194","datavalue":{"value":{"entity-type":"item","numeric-id":161641,"id":"Q161641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$E54B2984-3E8C-4DD1-ADD6-5EDDAB0479F0","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"391107ffc7a24346d69c573e292e4ff4587e3aaa","datavalue":{"value":{"time":"+1991-00-00T00:00:00Z","timezone":0,"before":0,"after":0,"precision":9,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q911245$701CB4C7-C9BB-49A5-83B9-F906C47F2BC5","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"286db0309cb041f9ed17a8d5ea58fadc58166113","datavalue":{"value":"An observational approach to the construction of implementations of algebraic specifications is presented. Based on the theory of observational specifications an implementation relation is defined which formalizes the intuitive idea that an implementation is correct if it produces correct observable output. To be useful in practice proof theoretic criteria for observational implementations are provided and a proof technique (called ``context induction'') for the verification of implementation relations is presented. As an example an abstract specification of (the algebraic semantics of) a small imperative programming language is implemented by a state oriented specification of the language.    In order to support the modular construction of implementations the approach is extended to parameterized observational specifications. Based on the notion of observable parameter context a proof theoretic criterion for parameterized observational implementations is presented and it is shown that under appropriate conditions observational implementations compose horizontally. The given implementation criteria are applied to examples.","type":"string"},"datatype":"string"},"type":"statement","id":"Q911245$5219CAC3-42D8-4951-B768-8ED15DC8DDC2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"092d9a7dfbbaaa84ba458f8d83190fce94c9aa54","datavalue":{"value":"68Q65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q911245$D57EF7A3-6EAB-4416-B935-AC55F492F7E9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"b8e3f40e3cc87753c4e0b7d7ce4bdc00805f626f","datavalue":{"value":"68N01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q911245$6902E59F-A27B-4C7C-83C9-0284CA4A31FF","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"909466204a13c746ce1019a47a15c586b09d0534","datavalue":{"value":"4141467","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q911245$E2ECDB84-3CB6-4D82-81EF-FC611A02323F","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"cf6483e93ff0b0b0a920caa3a8bcdc780bd2e5cf","datavalue":{"value":"algebraic specifications","type":"string"},"datatype":"string"},"type":"statement","id":"Q911245$37D17851-4D1C-42B2-9063-C15133849EE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"a513f23308cd4c9f3e30580425a006906167ed03","datavalue":{"value":"observational implementations","type":"string"},"datatype":"string"},"type":"statement","id":"Q911245$3C71CBDD-83C4-44F7-9881-F063566D93AD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"66824d9cf653f7dee3c76f98a8ea1aa06432fa7c","datavalue":{"value":"verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q911245$5394AA8C-4BF2-4CF9-B74E-F4105773686A","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$2997B91C-2364-4A11-BAF6-5A93F69FD120","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"3209dcffb68253e20194ca2da7f3cb7095c85efb","datavalue":{"value":{"entity-type":"item","numeric-id":801667,"id":"Q801667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$16B1CD02-8A81-42D3-8164-85A37193BB42","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"993a0290c8b5d5862b3c4459907f50d914c2e0e5","datavalue":{"value":{"entity-type":"item","numeric-id":3763565,"id":"Q3763565"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$FA23EA8D-59DF-4DAE-9259-10C24C12B593","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a6919ba84c94face972c4fcbaccdc5058745cefc","datavalue":{"value":{"entity-type":"item","numeric-id":3906394,"id":"Q3906394"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$2954DEA4-89B7-4896-9E43-80F0BE8C1000","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"52efcbbe11513c685db1a2de3c5505e7a27397a6","datavalue":{"value":{"entity-type":"item","numeric-id":3947104,"id":"Q3947104"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$89D873BB-47D5-4A2E-BC81-6CA130199506","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"35f820e9c2b45f8f035a710ad26c0ff0e5c7ae48","datavalue":{"value":{"entity-type":"item","numeric-id":3221381,"id":"Q3221381"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$C40B1C6A-55C9-4BFE-BCF1-9C05C25977C1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4dc01a28b8e042eaee4713d2ffe90785f0ff058b","datavalue":{"value":{"entity-type":"item","numeric-id":1163361,"id":"Q1163361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$B2626B26-39A8-4922-BE55-915B237F3F0E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7c017de94be929303e103db5a7762532c2f6325d","datavalue":{"value":{"entity-type":"item","numeric-id":4749185,"id":"Q4749185"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$BDDBE7A6-E7EC-4FF6-8D1B-3BA9AADCBE3E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"aee5e41dfac94580b32bca85e4ef53cf690e4af1","datavalue":{"value":{"entity-type":"item","numeric-id":3742703,"id":"Q3742703"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$648E2E6C-9EF4-4A85-8537-2F94DBED0F98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1f3813ab614a97a156330c623ed2e7bf909d45fa","datavalue":{"value":{"entity-type":"item","numeric-id":4105777,"id":"Q4105777"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$EE555596-2831-4A40-9766-9F45DF661BC1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f325c977c21595a567edfd399ff116dce390cad0","datavalue":{"value":{"entity-type":"item","numeric-id":3956373,"id":"Q3956373"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$075B9318-556C-44B9-9DBA-A6004AD03AED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f9c583b65c7819a91d7f03c50f27e11283eee826","datavalue":{"value":{"entity-type":"item","numeric-id":3962973,"id":"Q3962973"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$F01D75D4-B2EC-4AA6-ACD3-C6265403432E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5b4e8d326130bcb0b8a78ad9006b5a69e2c4773b","datavalue":{"value":{"entity-type":"item","numeric-id":3707384,"id":"Q3707384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$A7491EFD-A39E-43E7-BFCB-F60FF9C10189","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"01d1f0f5487f8c0ee42819e7149f6be853525c70","datavalue":{"value":{"entity-type":"item","numeric-id":4729318,"id":"Q4729318"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$99624B1A-FABA-4AB5-A399-ACB259BB94A9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13c8332b10186708c6708131542afb51481ba405","datavalue":{"value":{"entity-type":"item","numeric-id":3938468,"id":"Q3938468"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$9D801B09-154C-4BD9-B5A5-5D6C44F41D60","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4253d384646b019f04280faeb4984e28cdef49e","datavalue":{"value":{"entity-type":"item","numeric-id":3677153,"id":"Q3677153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$96D3A439-0B25-4A31-816A-6F1215EE4F6D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62461d4c2275b5c15065872b300e8488669b9d8b","datavalue":{"value":{"entity-type":"item","numeric-id":4721633,"id":"Q4721633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$FB47B4AD-6DB2-4D8F-AF11-C10977F3B42F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4e16f53aacdc2272655a20338ee20ff055417e6d","datavalue":{"value":{"entity-type":"item","numeric-id":3954805,"id":"Q3954805"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$3FC10502-FA1C-4DF8-9AD8-E09E5A6A7979","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"44b7f189eb7f5e56515006b2399dc063811b0064","datavalue":{"value":{"entity-type":"item","numeric-id":1080652,"id":"Q1080652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$E9F25153-EC0B-4809-89E8-ABC060600241","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b77f2e9aafcfe3d583d9c09d0768e0534ac2beee","datavalue":{"value":{"entity-type":"item","numeric-id":1050767,"id":"Q1050767"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q911245$7289A2A6-0FAE-459C-A307-172084402C78","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"f29c67dae6854583f6e61f9df984dac7fd67d947","datavalue":{"value":"https://doi.org/10.1007/bf01178505","type":"string"},"datatype":"url"},"type":"statement","id":"Q911245$9ED9DDE4-0155-4C56-A823-ED2F5143D398","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"496798b4125b0c056faac8bca4ee86e81c109b3a","datavalue":{"value":"W2062384035","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q911245$E2071CB5-80D9-46C7-958F-4BD0C06320AC","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1e7c5c7912240f30efed1d28918c75858ea45bd9","datavalue":{"value":{"entity-type":"item","numeric-id":5096143,"id":"Q5096143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c183ec0698937651ddfdaedf15904e606640dc83","datavalue":{"value":{"amount":"+0.954218089580536","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q911245$7DA07546-ACDD-4570-B167-16AC8323F1A6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"660b3719580fbe63dc866cdcce498cd70b924723","datavalue":{"value":{"entity-type":"item","numeric-id":1199928,"id":"Q1199928"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"56df0ca4f0fc416320173f391bca0b238642b0a4","datavalue":{"value":{"amount":"+0.8287546634674072","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q911245$8796AB72-F515-4888-98D0-1FEB3BE96FD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c64e0723d0382945f0fca295fe1f451178b5a2b0","datavalue":{"value":{"entity-type":"item","numeric-id":3780424,"id":"Q3780424"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c364cff908bb9ba4ce565f881ba23a61ef38ec97","datavalue":{"value":{"amount":"+0.8267369866371155","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q911245$EBC5685A-684D-4C2A-8D32-AABD765A4F29","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"219d4f8253339b4fa8333583dc7c3dea28c9049e","datavalue":{"value":{"entity-type":"item","numeric-id":3707384,"id":"Q3707384"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"fdad15a2bb5a4d87622af5749507f1e14e54f930","datavalue":{"value":{"amount":"+0.8059754371643066","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q911245$DCAF83F8-FCA5-468E-B54E-0D58C4F63671","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"44c0b247fdf32a6c29e6de07d9e661fb11c73f45","datavalue":{"value":{"entity-type":"item","numeric-id":1127821,"id":"Q1127821"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d9ca919183e4680b589b3daa8f314fc2509caaee","datavalue":{"value":{"amount":"+0.7953878045082092","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q911245$3BB283C2-7235-4423-A643-B0B0F00A983D","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:911245","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:911245"}}}}}