{"entities":{"Q1984797":{"pageid":1995539,"ns":120,"title":"Item:Q1984797","lastrevid":53704613,"modified":"2026-01-25T14:17:16Z","type":"item","id":"Q1984797","labels":{"en":{"language":"en","value":"An assertional proof of red-black trees using Dafny"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7187046"}},"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":"Q1984797$243B1923-D5C8-404A-BC81-899E94EB4E90","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"40200668ba5a1d16cb95ae8f76f4076a59ffcfd5","datavalue":{"value":{"text":"An assertional proof of red-black trees using Dafny","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1984797$C64A2575-2A39-443C-A887-980F1BD6DBA0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3e77fb5f22a1e20e2db8a670cf0d3a2e65c352e1","datavalue":{"value":"1468.68082","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1984797$91367E39-6888-4076-B6FC-CB6D55970F3F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b3c4f0a73cb16daf1a6d20b105b364dce4d8e5e0","datavalue":{"value":{"entity-type":"item","numeric-id":1984796,"id":"Q1984796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$A58547F2-C4E4-4D76-A4DE-BBF621092600","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$42AB3F65-1D42-4B97-AF93-4D7B4DCB187A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5583640b16c3225e3c55a84532f843da9ad4b6cf","datavalue":{"value":{"time":"+2020-04-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1984797$255184D3-2DF4-42F1-8966-5F02B25F254B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1984797$D2BB0BFD-0277-4FA0-B417-8FB78FA8A6B0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1984797$88B03FF3-D4F0-40BE-B5F7-AAC7CDC2F842","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"22c048f6c1a4450c6fdfd2a4af78da6f47e46ab8","datavalue":{"value":"7187046","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1984797$90A197E0-4045-4830-BFC0-ACD508C2909C","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"43d8de44b3f88bd19a871628a3509981cd748562","datavalue":{"value":"data structures","type":"string"},"datatype":"string"},"type":"statement","id":"Q1984797$FDBBF962-4B37-42ED-874F-FE51360E28F7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f864626b47de03bc550dfb512336687f3eaf0bee","datavalue":{"value":"balanced trees","type":"string"},"datatype":"string"},"type":"statement","id":"Q1984797$43231024-1A42-4AA5-AEE2-022930533505","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ae1dce7d5fb5bc7b29af8b5cf5ad73f30f632fed","datavalue":{"value":"verification platforms","type":"string"},"datatype":"string"},"type":"statement","id":"Q1984797$F46CE9B1-9DBA-4FF1-A5ED-5637492B7768","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"91328e3ac5dfce9b45d01b607b8d8c272a5b6733","datavalue":{"value":{"entity-type":"item","numeric-id":14670,"id":"Q14670"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$D4802EF3-639D-46C7-A867-451D7207A2CE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"602b32d79a3dd12c7713e80fb0597b8ab4375f08","datavalue":{"value":{"entity-type":"item","numeric-id":16614,"id":"Q16614"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$FD80F137-72BE-4591-AED0-79EBA8C73D5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$D127B5EB-EABF-42E3-B3E8-845FD9BBB06A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$18F86664-BFE5-4BEB-A49B-D2F5E49D3A19","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"b6da1f42e3d4d28e24ecb68672c28ee0982a60c2","datavalue":{"value":{"entity-type":"item","numeric-id":12950,"id":"Q12950"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$94E39D00-A6D9-44CB-B407-5A313C01E341","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"875fd2341d7eaef60a26a549ea0c9adfdf328e2e","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$8D622F9A-9F27-4D29-85C5-06AB2CDAE10D","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":"Q1984797$E3F32EC5-0F6C-4569-BC8E-EC94417E93FE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"8f32b33e3bd4dd46df7adb11db51021ec66a0994","datavalue":{"value":"https://doi.org/10.1007/s10817-019-09534-y","type":"string"},"datatype":"url"},"type":"statement","id":"Q1984797$42E82034-4EF3-44E0-86B8-7804EEA8810D","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"f3154510358df224dbd57248186aeed45e6839f6","datavalue":{"value":"W2977551386","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1984797$015B251C-F766-4D0C-A002-A778F5EFD626","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"6da661f3e4df22c235922501a4b681304f201c12","datavalue":{"value":{"entity-type":"item","numeric-id":5060098,"id":"Q5060098"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$619E58FC-AAE4-48DD-AC7C-9FB1F628964E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3d4a4b9328aeaa198621796249011494635ff553","datavalue":{"value":{"entity-type":"item","numeric-id":2551313,"id":"Q2551313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$C3A15387-C109-4790-AA6B-7294844F523E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ef146def2d585ff66e37bf85e5bd822184c47a27","datavalue":{"value":{"entity-type":"item","numeric-id":2549238,"id":"Q2549238"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$FC4C8099-32FB-4E85-98D0-81A04F085DAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f3ea02b15a15931f4cd364dd4a0ce61e10ac225","datavalue":{"value":{"entity-type":"item","numeric-id":703860,"id":"Q703860"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$FDBD79C7-5BBF-48CB-ABDA-16D2EE3B79FE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3bffe48c7c76b90bf68970921698e19786e1600b","datavalue":{"value":{"entity-type":"item","numeric-id":2747613,"id":"Q2747613"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$A44D51BD-ACCE-4740-8245-D09EED402DAB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"98589d6fa667da17f782a55cd2dc8c33d4dbf671","datavalue":{"value":{"entity-type":"item","numeric-id":5308710,"id":"Q5308710"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$886D0770-85C9-4DBF-A27C-6279EFFD7828","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"093682f82b55047546d767040082e61c8c07c786","datavalue":{"value":{"entity-type":"item","numeric-id":4282672,"id":"Q4282672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$D27982D3-44CA-405F-90C4-26FE1989B6F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1807204606c08bc0647f8c538053670a3e876b3b","datavalue":{"value":{"entity-type":"item","numeric-id":3066108,"id":"Q3066108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$F2D5742D-79C4-4EA7-9DE4-D0DBE4AB5037","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6ceb17906c1b4b968efa20ac5cef11ba46123bb6","datavalue":{"value":{"entity-type":"item","numeric-id":5277907,"id":"Q5277907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$CA573A83-1AF6-4703-9C8E-821AD253E19E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"561c39284ec9421bb8483b2aeef47c80a5eebeb1","datavalue":{"value":{"entity-type":"item","numeric-id":2829265,"id":"Q2829265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$A9E4E609-1F3C-40EA-BD7F-1213E5418750","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$3D857B36-8466-487B-BD68-A2703D6FAE34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"03e7885d0b3f4cd1fbf1726fc03e41b3124fca4a","datavalue":{"value":{"entity-type":"item","numeric-id":4943361,"id":"Q4943361"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$D45BC5B9-D18E-4031-9E1D-58BDC9F3D70A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2e00db80b77d8200c404d1a2e8fc24d94da053bc","datavalue":{"value":{"entity-type":"item","numeric-id":1193748,"id":"Q1193748"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1984797$ED43A22E-9AB5-4F15-B99E-17148BA822EB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c27fa964ae891e596a4c10b9236468e5d082f811","datavalue":{"value":"10.1007/S10817-019-09534-Y","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1984797$93A5A171-F0FD-4F01-9E29-ECDC72666F3B","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"15b2d8efc095f44c21690e6cc59d92f922b782e9","datavalue":{"value":{"entity-type":"item","numeric-id":2829265,"id":"Q2829265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ca0e09255f6926af508042faf827fdd9ddf1383a","datavalue":{"value":{"amount":"+0.7428431510925293","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":"Q1984797$5EDD70C8-E23C-47F8-A30C-BE4D9535C742","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"85d2ea3cd98365ad96a31aff0fee17031404a04e","datavalue":{"value":{"entity-type":"item","numeric-id":5434520,"id":"Q5434520"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6dcec586917848aa68dda8022d2b9df951c91315","datavalue":{"value":{"amount":"+0.7406565546989441","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":"Q1984797$A379616E-EF60-40D1-9D5F-79DD222C00F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"40fc5e7043528b48f48513ad3d7973b2a19e7a49","datavalue":{"value":{"entity-type":"item","numeric-id":5056001,"id":"Q5056001"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"410b9f7e2544de7d37d168eece2820cf36d43e79","datavalue":{"value":{"amount":"+0.7342979907989502","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":"Q1984797$6637B7B8-32C6-4011-BAE8-A80F03435AE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"cb66f5ed642237465bd4bd33f771eb4c0c5586c3","datavalue":{"value":{"entity-type":"item","numeric-id":2757083,"id":"Q2757083"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"7fd6a8c8747f0c0472b932031562b5825ab1396b","datavalue":{"value":{"amount":"+0.7279610633850098","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":"Q1984797$D8E69CB9-3224-4B0B-AB5D-C2A4990B8868","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24ad6160359367d315465542a8055f597ea93122","datavalue":{"value":{"entity-type":"item","numeric-id":2942864,"id":"Q2942864"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9da41baa355b2f5df85235e861332cb728093f74","datavalue":{"value":{"amount":"+0.7230959534645081","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":"Q1984797$80915961-83D8-4013-A70B-921C751E6CB2","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1984797","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1984797"}}}}}