{"entities":{"Q3216113":{"pageid":3226821,"ns":120,"title":"Item:Q3216113","lastrevid":87944024,"modified":"2026-06-04T13:13:54Z","type":"item","id":"Q3216113","labels":{"en":{"language":"en","value":"The use of hoare logic in the verification of horizontal microprograms"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 3881856"}},"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":"Q3216113$912274A2-1B1B-4226-A7B3-A902A42626E4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"035b30f33c800432707e94bebb2b83437227eec2","datavalue":{"value":{"text":"The use of hoare logic in the verification of horizontal microprograms","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q3216113$60992CBF-320A-43D9-9279-811BDD8D36D0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"a0f9f106f883c00281f5a2d31aeb86c4059a71c0","datavalue":{"value":"0553.68007","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3216113$7FA70CE0-C720-47E3-B24A-5B7BEBDC00BC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"ff575cbb2d4b6887d1fc350c3c3d38c0e20beef5","datavalue":{"value":"10.1007/BF00985823","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3216113$40D9CE86-31F1-49B3-B3C1-DF11B31B814C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"ad3cd5c6595aa0f3362f2e563c27a9dc2fa39e96","datavalue":{"value":{"entity-type":"item","numeric-id":1217592,"id":"Q1217592"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$E9D6D0DE-7765-49F6-A478-BE59564415F1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c145ed40ffcabf573ccc0e287afc84e81635ce77","datavalue":{"value":{"entity-type":"item","numeric-id":1309232,"id":"Q1309232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$DF960952-B06A-4C3E-81BF-96ABC864E602","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"299c62a7bb9adc9e73fd7facae1ee9d7ae362535","datavalue":{"value":{"entity-type":"item","numeric-id":2855323,"id":"Q2855323"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$351A6A82-A24A-4EFB-A5DD-A1B3CD5D74AA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"2ee0f220147ae8bc749a64db56839865dbc4f127","datavalue":{"value":{"time":"+1984-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":"Q3216113$FCEE6A41-45DE-4CE5-BE85-F00B07EE8597","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3216113$C270C649-1A00-427B-BD83-3613367DD900","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"169c817e93f9b7441a867f7f63c17f637e82bab1","datavalue":{"value":"3881856","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3216113$38E42FDE-48BF-4FA7-9244-5476C968EEA4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c77a366687df2fcc42fcc5ed4cbadd7a7723cba1","datavalue":{"value":"correctness proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q3216113$7EAE0712-7FC1-4AFD-A9FE-E789C1AC1728","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3216113$9FE57786-B149-4962-8AC1-5C07C489DB70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ac52900f9c775a1c2e9b77521a060cf4681ca7f4","datavalue":{"value":"hardware verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q3216113$34FFF6BF-AF4B-4E7A-83DE-DC83C243BAE4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe7a70b830f3bd9968ed6f86bdbf5f6726fc100a","datavalue":{"value":"microprogramming languages","type":"string"},"datatype":"string"},"type":"statement","id":"Q3216113$3F7242DD-F8E6-497D-AA1C-A9B49D0E6853","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"0e2869620dc874f5c5c63a0671e4acedcf219788","datavalue":{"value":"formal verification of microprograms","type":"string"},"datatype":"string"},"type":"statement","id":"Q3216113$137CBF41-8BC5-48DD-BCE9-DCECC86F099B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"3aa068fb5411c5ff15168e2790cf26498f299277","datavalue":{"value":"Hoare's inductive assertion method","type":"string"},"datatype":"string"},"type":"statement","id":"Q3216113$13EDD5DD-72D8-4CEB-86F1-A8B04B51CA18","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"1220fb887fe493572b2cc5d47c80ec30ffde5a46","datavalue":{"value":"horizontal microprograms","type":"string"},"datatype":"string"},"type":"statement","id":"Q3216113$E69E0C66-0FF3-4E10-BE78-A7DDA6FBFF99","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":"Q3216113$E62DBBC2-F788-47FE-968A-10F310D8EE6A","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"8fecd5c8dfb12e0e2530dd99ad3679ce7b307c38","datavalue":{"value":{"entity-type":"item","numeric-id":3923568,"id":"Q3923568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$4BE6A53E-440C-4899-9EDE-9E49878F7DCC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e068df1bfe0078e06a881ed61f8b1e26e5228e33","datavalue":{"value":{"entity-type":"item","numeric-id":3914396,"id":"Q3914396"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$E07C2A03-E174-4E9C-B4B5-F518E578AE21","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"323dbd6fd6973b3663055cf97da83be885dd9ec7","datavalue":{"value":{"entity-type":"item","numeric-id":5569944,"id":"Q5569944"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$CAE6943D-48DE-409D-BAC2-883190124D7D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4c6e079ea921bf39ce20b78c12e08a43b8a07ab0","datavalue":{"value":{"entity-type":"item","numeric-id":5621929,"id":"Q5621929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$E09A38A3-CFD8-489E-9D29-12380F451069","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d5db4cd80de0c2d5b3b19e4a746246d0f78c5501","datavalue":{"value":{"entity-type":"item","numeric-id":4076753,"id":"Q4076753"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$D3076BFE-3551-4FC7-8728-A455C00A99BF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"67b8a6374b4fc895d89506f759c76e54380f8254","datavalue":{"value":{"entity-type":"item","numeric-id":4144755,"id":"Q4144755"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$4F9F3558-BC93-4256-81F4-26B698E7AA1B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e47b8c90d45ee285590b1a168a8503851fe5b134","datavalue":{"value":{"entity-type":"item","numeric-id":3925859,"id":"Q3925859"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$3675766E-92D9-4E56-B36A-D515A5EF583D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e5285d79fb0a54034a765cc040755038d6ec0aeb","datavalue":{"value":{"entity-type":"item","numeric-id":2560721,"id":"Q2560721"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$051D1F8F-E83E-4220-A360-5CA0EB5323D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"43522741a5881651813aecfed6b174a4b945638c","datavalue":{"value":{"entity-type":"item","numeric-id":3969890,"id":"Q3969890"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$B528ED39-5E62-403E-8653-36A242887720","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"796364eeefb9789a01eab3a144d0337d6c23ee01","datavalue":{"value":{"entity-type":"item","numeric-id":1219675,"id":"Q1219675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q3216113$2D752CAD-DD9A-4C66-818F-4EBB707CF1D5","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"119c3e525f702051f5c79f8c370a147e944da9f4","datavalue":{"value":"https://doi.org/10.1007/bf00985823","type":"string"},"datatype":"url"},"type":"statement","id":"Q3216113$BCAB824B-6028-4D4B-8279-B48A626B90E0","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"bc001ffd5b1b653643dc3013437f7d03dac80343","datavalue":{"value":"W2028992386","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q3216113$B7C3028A-B044-4034-8549-7288FCDBF9F8","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d3e04b345d9e77db952c002ff6a36c8e6c848248","datavalue":{"value":{"entity-type":"item","numeric-id":3777442,"id":"Q3777442"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4691450f75025b581614e476b9dba5de2788293b","datavalue":{"value":{"amount":"+0.7831343412399292","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":"Q3216113$F61DB85E-F113-48A9-91C3-E91DA66D959B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d21618c33755d34119c83c7d442dd2530ec4786f","datavalue":{"value":{"entity-type":"item","numeric-id":4004176,"id":"Q4004176"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"264f3afda8c2c8c820cbc67da254cf071b5b66c3","datavalue":{"value":{"amount":"+0.7404702305793762","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":"Q3216113$6ED109FF-D38A-4984-AB8E-68C134C5B627","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"286621dceae39ed4c4865eaae2eefab2f27b11b1","datavalue":{"value":{"entity-type":"item","numeric-id":1316958,"id":"Q1316958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"264f3afda8c2c8c820cbc67da254cf071b5b66c3","datavalue":{"value":{"amount":"+0.7404702305793762","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":"Q3216113$7F499D6B-1D7C-47F9-AA4D-F0D2CB6DD2CC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"bb57dac5e9733bbbaad6a936013c102dabfd2939","datavalue":{"value":{"entity-type":"item","numeric-id":4419604,"id":"Q4419604"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"886c59b3305a5e893319d218a71b064e54f242c8","datavalue":{"value":{"amount":"+0.7285616397857666","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":"Q3216113$4F828473-81AE-423C-947F-B9367EE2DFD2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2a86794cf4076c68faa757aa8a6ee19590f4c951","datavalue":{"value":{"entity-type":"item","numeric-id":1122998,"id":"Q1122998"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"24f127436d611790020780a6609bfbc3c8e5b36f","datavalue":{"value":{"amount":"+0.7107512354850769","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":"Q3216113$C9CBDC26-7969-49D8-BF6D-436F97C21CE8","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"The use of hoare logic in the verification of horizontal microprograms","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/The_use_of_hoare_logic_in_the_verification_of_horizontal_microprograms"}}}}}