{"entities":{"Q2994490":{"pageid":3005214,"ns":120,"title":"Item:Q2994490","lastrevid":45215620,"modified":"2025-12-03T09:23:33Z","type":"item","id":"Q2994490","labels":{"en":{"language":"en","value":"Proving Quicksort Correct in Event-B"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6608402"}},"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":"Q2994490$E760C79F-BA58-4201-A1F8-3214D79652D4","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"7851d86b7e2d42f442947274a2ceccb4993b5cce","datavalue":{"value":{"text":"Proving Quicksort Correct in Event-B","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2994490$F91DE8A9-49B6-4A95-A9B9-AE2D1EC6CF6F","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"2aa847f0ef16a873c76b283ebfd4d389aa457162","datavalue":{"value":"1342.68114","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2994490$50875CBC-9424-4B3C-8F54-21E7D7F3BA21","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"7c3cadec2ef714e5660771f9ec0500ac9b16a25e","datavalue":{"value":{"entity-type":"item","numeric-id":432153,"id":"Q432153"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$70BD86AE-9102-412D-99F1-24FE28B06063","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"3478ec308a15597e43cb648673c843463f4d3028","datavalue":{"value":{"entity-type":"item","numeric-id":163528,"id":"Q163528"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$ED09F13D-0DD0-4C09-9C5A-DD2AD79A044E","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"54b54adebb79dfabd07c0151545b3468c800875b","datavalue":{"value":{"time":"+2016-08-01T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2994490$D09E69F3-1CFD-4E01-B963-BA51D96E020B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"3f97694d44af155a68434cb72eabc6a4d5dd5227","datavalue":{"value":"68P10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2994490$D1E0BD26-D34D-4B62-B9EE-BC347EE00110","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"c675b8a733d5d59e82381336a3020799ad092ec5","datavalue":{"value":"6608402","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2994490$60BC7E7A-FCB9-484C-BF74-E010662088D5","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ab20a0363e682206851b94b3be1e96bb56399f58","datavalue":{"value":"refinement","type":"string"},"datatype":"string"},"type":"statement","id":"Q2994490$CA64BBC5-B386-4929-84B0-C84A3470FA0D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c50d987ab7c3ea2a41cb6aca681d912964971ed8","datavalue":{"value":"program verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q2994490$026719C1-4463-4D55-9BF7-006A0A32E1C5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"9d090cd3495c3058b4c58f325c991462c282a60a","datavalue":{"value":"Rodin tool","type":"string"},"datatype":"string"},"type":"statement","id":"Q2994490$97A89C0E-E2DC-46E7-B40C-7F015D24ADB3","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"9189048b3936abda7e80b02cf829681849623735","datavalue":{"value":{"entity-type":"item","numeric-id":33628,"id":"Q33628"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$3FF9578D-857A-421A-9022-FF820CEA74EC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3dcf6ea9ac65c890e0513ced8e4b0dde71e50b0f","datavalue":{"value":{"entity-type":"item","numeric-id":19141,"id":"Q19141"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$6104BCA1-A382-4826-B87C-2BFCBAF8C6D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"e751138e8b150b28783c5a210048f6817120432b","datavalue":{"value":{"entity-type":"item","numeric-id":32511,"id":"Q32511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$9E9EFFC5-F872-4194-B58D-ED01F0E5E8D4","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":"Q2994490$EEA887F2-5930-4038-9327-E83FD9E50C9C","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"9cd3c5f08e91b0bdad8637bc7b9c23a9e78a2c62","datavalue":{"value":"https://doi.org/10.1016/j.entcs.2009.12.017","type":"string"},"datatype":"url"},"type":"statement","id":"Q2994490$86121EB8-DC1A-4614-8BDB-004F050F5479","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"be1584ac27f784ad1581df5e368ecc1bc7f31db9","datavalue":{"value":"W2031664756","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2994490$E1B49F94-44EF-4A46-A298-255812BBE290","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"ae170f67b5a99f655b51707d2e6917e4913c4d7a","datavalue":{"value":{"entity-type":"item","numeric-id":4208552,"id":"Q4208552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$1B0C5913-995D-4F7D-B726-8EE905319552","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a64dbb7c90690de5fbdf0d30d9b861ec41a32a6","datavalue":{"value":{"entity-type":"item","numeric-id":3569584,"id":"Q3569584"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$C9654975-AC18-4EFF-9219-0134B0988519","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b9ebd97ebad7f6b6543ac93ba5957bb5f6f50160","datavalue":{"value":{"entity-type":"item","numeric-id":5703804,"id":"Q5703804"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$6D8E718C-F025-486C-9F22-6FC3ABE52C2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"e8e7b9da18e16cd970511c07ad5cdb803278d984","datavalue":{"value":{"entity-type":"item","numeric-id":5294155,"id":"Q5294155"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$8102E777-80AB-4022-A31B-FFC89515DDDF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"989ffcc992d1ac31e39a63758614d7ce6f35323e","datavalue":{"value":{"entity-type":"item","numeric-id":837527,"id":"Q837527"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$9A89BA67-4A3A-4141-B3D9-1AC2A945F120","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8773a932431602bdddce87be2ab32e5880c2dfc2","datavalue":{"value":{"entity-type":"item","numeric-id":5639351,"id":"Q5639351"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$9C66A77A-D088-4488-832E-D10D51A3F238","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"457e380a94d38fe11d0c65a23c879f3ba8179626","datavalue":{"value":{"entity-type":"item","numeric-id":3535369,"id":"Q3535369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$2E15C531-CA4E-4AE1-B8DC-AEE0CCB7D6CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a98e1d68003b0040c15c163e66f3fd9578fb9386","datavalue":{"value":{"entity-type":"item","numeric-id":3997074,"id":"Q3997074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$77ECAE6B-0B6F-4607-9601-EF49F40EE6B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"992009231a3ccf90d1f1c83b557e5dfa4622a42d","datavalue":{"value":{"entity-type":"item","numeric-id":921907,"id":"Q921907"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$B00C9533-93AF-4887-85EE-2EBFB6F27A50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"768da93377b5dbe67ffc466d796d0d32932c2d63","datavalue":{"value":{"entity-type":"item","numeric-id":4301161,"id":"Q4301161"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$59C4A705-A660-48BD-8FD5-6DA204E56CB3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fc019e2b4d5136976181164b24b3484dcfaaead6","datavalue":{"value":{"entity-type":"item","numeric-id":4808845,"id":"Q4808845"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2994490$0E705086-2A8E-4A3A-B4FF-F6400DDC63F3","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"cde9a8eac36e89bf2104cdf8db1509e0b43c2931","datavalue":{"value":"10.1016/J.ENTCS.2009.12.017","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2994490$D9C09C74-021C-4FFB-AEB2-1522AD82A928","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"3fa45e1720565714eacb2a6ab9a8ca046e7056bd","datavalue":{"value":{"entity-type":"item","numeric-id":2026813,"id":"Q2026813"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"f9dfc2d5bbf332e56b3fb824aa0b436b7522e90c","datavalue":{"value":{"amount":"+0.8442919","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$64D312A9-E634-4E39-AC36-E8850CAB4373","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5b5408e13c72013dbf0518d9f7816f407facd01b","datavalue":{"value":{"entity-type":"item","numeric-id":5020652,"id":"Q5020652"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9c9fe766d43227d13dd1d7b439216a237af17922","datavalue":{"value":{"amount":"+0.83886653","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$A3FAFBC6-3D1F-4BB6-880C-C2AA7EFAE051","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"6bfb3edc799c6bdc6c0d01c229e6380861e83c87","datavalue":{"value":{"entity-type":"item","numeric-id":2445402,"id":"Q2445402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"824221b8c70db6e95bcfbd4c0c579e17121648ac","datavalue":{"value":{"amount":"+0.82959414","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$C3C60F6F-DC4C-4666-88EC-BA307CA28668","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"551f66a7093503e5bd660f45a7f898f4d86d64fe","datavalue":{"value":{"entity-type":"item","numeric-id":1630025,"id":"Q1630025"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b9d8f0802de636b9dfbe174bc4560f7334dc08cf","datavalue":{"value":{"amount":"+0.82292664","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$7B2B2FCB-8A12-4507-8C8B-06F866ACFFF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"60602316023f75163a19dfb79df665cbdd787249","datavalue":{"value":{"entity-type":"item","numeric-id":1096378,"id":"Q1096378"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07e6ce2fe614232902ba09e19f7572d1f543a039","datavalue":{"value":{"amount":"+0.82145095","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$77B4034D-E51F-4E21-9CA3-D4B3D534F946","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5e47c6c231418b2d8168867dcb6a3ec1352e587a","datavalue":{"value":{"entity-type":"item","numeric-id":3638257,"id":"Q3638257"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b6cb2ce437c8051dec40d6b516908466c3bd7220","datavalue":{"value":{"amount":"+0.8213972","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$842D2BF3-9CC9-4F62-AB2E-0ACC12474A13","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38ca397ea0f0672e79958ca397a8c463ce33709f","datavalue":{"value":{"entity-type":"item","numeric-id":3809239,"id":"Q3809239"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ba53012b028d81ee0aac653cae91c3f0c8853eed","datavalue":{"value":{"amount":"+0.8166235","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$CE5E661B-2B76-4D06-AE78-05946424D705","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4f9c84dcbc86a88bd281f6ffd7b4b3bfae4d21ec","datavalue":{"value":{"entity-type":"item","numeric-id":5049010,"id":"Q5049010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"720e41fd561469a2111fa97dc376b0b4a937b518","datavalue":{"value":{"amount":"+0.8139695","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$A38EA37A-F771-4DCB-86C9-FFBB0D1F9CBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2cbb7497e836b55cf2564021ce63cc26fbee944d","datavalue":{"value":{"entity-type":"item","numeric-id":2968412,"id":"Q2968412"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0d366ffcd9d5e1e58086af8e12758a1d25489fc3","datavalue":{"value":{"amount":"+0.80936325","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2994490$F97293F0-2937-475A-B2D1-71626837B5F5","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:2994490","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:2994490"}}}}}