{"entities":{"Q5045478":{"pageid":7075055,"ns":120,"title":"Item:Q5045478","lastrevid":54435692,"modified":"2026-01-26T19:49:30Z","type":"item","id":"Q5045478","labels":{"en":{"language":"en","value":"Hoare-style reasoning from multiple contracts"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 7612681"}},"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":"Q5045478$F54E05FD-3A03-4E07-80D9-D678547879DF","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"53a536e9b321b1bc3425c8b7d8058ee626ecab65","datavalue":{"value":{"text":"Hoare-Style Reasoning from Multiple Contracts","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q5045478$A284F39B-CC78-4054-A446-C2C0E2214CD0","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"cf73bb575eb566b1f37fc21662aa95887fe90b08","datavalue":{"value":"1498.68168","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045478$DFC1FE77-8FE9-45D3-8444-332258D2A8AB","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"f42d4848afd565a93ebfb684345b74839bcb2ed4","datavalue":{"value":"10.1007/978-3-319-66845-1_17","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045478$3C681B00-3FD9-4F53-947A-014A8F2DD06C","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"49a3a8c4e00dcbc97f85642c2695ec01433ebead","datavalue":{"value":{"entity-type":"item","numeric-id":444465,"id":"Q444465"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045478$256D62B2-8D4E-40C7-9C87-89A421E8CD68","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"0723c8f5d576e86addcbab47e54c9c5955c26304","datavalue":{"value":{"entity-type":"item","numeric-id":1648641,"id":"Q1648641"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045478$04F9A489-6746-4967-96A4-274A8419EA14","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"1289b2caf6e863cbdf35bed097df9cc33ff8c470","datavalue":{"value":{"entity-type":"item","numeric-id":2141288,"id":"Q2141288"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045478$DEA40E61-96DC-451A-B2A8-B19785EA8992","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"85c07c7737819bff773f78e2590a3bb761fe677b","datavalue":{"value":{"entity-type":"item","numeric-id":162374,"id":"Q162374"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q5045478$5C1E6950-7E00-4756-8C77-4F403058C9AE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"96420cb12347695a963e770401ec584dde3a55d6","datavalue":{"value":{"time":"+2022-11-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q5045478$9893F474-030B-4301-AD9C-0955DBEDC049","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045478$C0528F90-D6D5-4A20-B164-6CB4E1BE6FDD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d53cd5ab715340bbfc507bf5b4aac1b907f4465d","datavalue":{"value":"03B70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045478$9457A742-169A-4A53-8AE9-8D902E57746F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045478$20A0A4F7-52AC-4F5E-B257-C31FB8E39D25","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"a372bfa70142de45eb6f636804c0de9a96e7931f","datavalue":{"value":"7612681","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045478$EB3A476F-BD70-4467-B5F4-0EFF9F9B7C2B","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8649681bd6e022af57b527d538b7a92c7e6b6e88","datavalue":{"value":"Hoare logic","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$074B6934-A315-449B-BF39-55350A62EF65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"de69df0aebf5634f69f5d335c7ccf65f7582db5b","datavalue":{"value":"multiple contracts","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$2DB3EC79-064D-40B2-98A0-CC1FCFEA55A3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"8d81fe775bcf973a3569dd9a88e27228e05a3a9e","datavalue":{"value":"contract-based verification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$B9C37BC9-6755-4419-95C0-471AE4EFCD6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"c2de1fadf1eb60da024aa33059889b77bcc7a097","datavalue":{"value":"contract-based specification","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$0014FBCC-2DEA-49DD-AABB-31AAE098D695","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"92c22d8cb5322dc118d1b0dffa993c70bd638181","datavalue":{"value":"adaptation","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$AC8F8E23-38CE-47BF-AA08-2C785D9EF22E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"acc1a615ddbbf6c3341d48b3a082cfcf5c325348","datavalue":{"value":"unavailable source code","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$EE751A75-C32D-475B-B00B-D8D4CE179C45","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"fe51228e17b836f3520db7bc0de40e5086eebee3","datavalue":{"value":"soundness","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$18332553-A964-4544-8029-8D32754DD1D5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f6816fdf79dd11ac09d9af4886c02baab03d2cf9","datavalue":{"value":"completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q5045478$B3EAD63F-FA9E-4812-8D90-C0A9B9538A38","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":"Q5045478$5771E8B8-1612-430F-B47B-E43186365EAE","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"285674a2c6c71ad54865ce86fcf940aea0f281ee","datavalue":{"value":"https://doi.org/10.1007/978-3-319-66845-1_17","type":"string"},"datatype":"url"},"type":"statement","id":"Q5045478$6F168D61-E500-4C96-AAE6-CC8632820E68","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"6ff1b63ce14c0e5eabb9163b07dcdc70fe2568a3","datavalue":{"value":"W2747300583","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q5045478$92B4BC07-5A75-4227-8502-F660A12CF450","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"4cb59c78b4322b377b80c979b25f8ee3e7075c9b","datavalue":{"value":{"entity-type":"item","numeric-id":4928448,"id":"Q4928448"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"266ebea0683b9b43bef89ea5910c8ebd53c95dcb","datavalue":{"value":{"amount":"+0.7263647317886353","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":"Q5045478$4572E5B4-67DD-4FA1-90BD-4366299C3829","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0d83f355a39bad1a41fd205089ab9576891a5854","datavalue":{"value":{"entity-type":"item","numeric-id":2044183,"id":"Q2044183"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6a5352dc308f34890292968fad8bdddbf558652","datavalue":{"value":{"amount":"+0.7011637091636658","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":"Q5045478$C0E18338-5F41-4C62-93BA-7DF58882ED81","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9b19db6cec98dba3f3442445dac462f86c273edc","datavalue":{"value":{"entity-type":"item","numeric-id":4632313,"id":"Q4632313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"227d28743be114986b85eed0ce6c73bf2e0c4e86","datavalue":{"value":{"amount":"+0.683380126953125","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":"Q5045478$2019A179-130F-42BD-8FBB-C25930CE1D05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"849f75c5a6e8b0c6538786d519488b33480e2443","datavalue":{"value":{"entity-type":"item","numeric-id":2038040,"id":"Q2038040"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"b397a0564452ba835b1ddb40746a2075fdc329d9","datavalue":{"value":{"amount":"+0.6766847372055054","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":"Q5045478$3847849E-221D-45E6-B08E-996F47B6764C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"d19e005a0abe117167f38c3b5f5143e8643419a6","datavalue":{"value":{"entity-type":"item","numeric-id":604392,"id":"Q604392"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77a1474d4a01b606f950a951a8d9692fb30b6520","datavalue":{"value":{"amount":"+0.668952226638794","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":"Q5045478$2F234415-19A4-4665-95D6-C72A59937FD7","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:5045478","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:5045478"}}}}}