{"entities":{"Q1262115":{"pageid":1272865,"ns":120,"title":"Item:Q1262115","lastrevid":68322957,"modified":"2026-04-12T22:56:16Z","type":"item","id":"Q1262115","labels":{"en":{"language":"en","value":"A proof rule for while loop in VDM"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 4123274"}},"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":"Q1262115$438086D9-B9AD-4EFE-9DED-4EF0C0C49D3F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c95199a63435fa502c986cd2618120ef52dec119","datavalue":{"value":{"text":"A proof rule for while loop in VDM","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1262115$5DE6CA8D-4BF9-431B-8E7F-430B44739AC4","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0d5edba44c5f073fef1d27b40ea7825d99267264","datavalue":{"value":"0685.68020","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1262115$60CACDF2-BFEF-4EA0-BF2D-6380ECBBBF7E","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"409d92188e60b6b5229829be4d3e8ada5a1aface","datavalue":{"value":"10.1007/BF02943366","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1262115$EE75ADA3-3660-425D-B79F-6B34F7D4A933","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"f34b89e30b0e9b69a017ca336115da3bc6513327","datavalue":{"value":{"entity-type":"item","numeric-id":1262114,"id":"Q1262114"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$61D9AFCF-F142-431A-B996-B2EFA94CBE20","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"3e04b57d9d645daf52220642c477e0f1ba2c93b4","datavalue":{"value":{"entity-type":"item","numeric-id":192541,"id":"Q192541"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$4D64F37E-BAE9-471C-ABE6-B00552F7FFEE","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"4c3c57bd2a24956e0520aebbb172d094d92623f1","datavalue":{"value":{"entity-type":"item","numeric-id":182337,"id":"Q182337"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$75EA99E3-C7DB-40EF-B62F-2700F9532ECA","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"7211ad5ca16eb0d22cd0051fff3d0f3af254ceb6","datavalue":{"value":{"time":"+1989-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":"Q1262115$90F25BDC-1E97-4DC9-A7B7-DBA6458DDE94","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1262115$A9DDE501-3CFD-4924-8F8D-C31CD65934BE","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"51c295f3cb4653ef3bd8c8c935f26f19d9cebe79","datavalue":{"value":"4123274","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1262115$09C276D1-FF47-4665-A768-5B88BA733FB3","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"94d05492a0435675532bbf6e3f062cf5f6fe0849","datavalue":{"value":"VDM","type":"string"},"datatype":"string"},"type":"statement","id":"Q1262115$D2B56ECB-77A6-42D4-B079-3B279F36A73B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"13c7bf0c237ed21b77cc6202408672691e8e8e93","datavalue":{"value":"two-state post-conditions","type":"string"},"datatype":"string"},"type":"statement","id":"Q1262115$919E112B-8AF0-403E-95F0-91261CC35171","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":"Q1262115$17CFD518-0087-4A80-9BF5-216AD2EDC88E","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2f9e6cf81b9223fc423cae2caf64aee0a427a0c","datavalue":{"value":{"entity-type":"item","numeric-id":3038590,"id":"Q3038590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$07066676-C5BE-4C1E-9C42-AAD171DDEC79","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":"Q1262115$ACA9B68B-EC48-4818-BE1C-665014C566B5","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":"Q1262115$2F47E057-7B6A-42C5-A597-E3FDCE844747","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c82ad10c73e928271f482901deda0f097caa8289","datavalue":{"value":{"entity-type":"item","numeric-id":3723675,"id":"Q3723675"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$0F5484AE-F6C5-40AC-80F8-19964591E5E7","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":"Q1262115$42ADC07E-CAAF-49AB-BF5F-4F248B96506B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"18ac860696e668a9ea3bf009a3485e439b6a4bbd","datavalue":{"value":{"entity-type":"item","numeric-id":3859249,"id":"Q3859249"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$E4426A48-3ACF-40E4-AAC7-F31A2DE51370","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa95e3f926378ec692a2f5af0f0675c611c5d525","datavalue":{"value":{"entity-type":"item","numeric-id":3729999,"id":"Q3729999"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$AE09D42E-BD9B-445B-BFA6-F5094E24ACB2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"83e646822c7e8f7e68867ade26f59c8b15d8260c","datavalue":{"value":{"entity-type":"item","numeric-id":3707340,"id":"Q3707340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$4B24A684-36AA-4330-BC96-15EDA190BDB4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"9cc2ea361e1855c36da932752239c9c0ca7fba47","datavalue":{"value":{"entity-type":"item","numeric-id":3028331,"id":"Q3028331"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1262115$5A25C5E8-547D-4923-8B2D-C4D1E3909F31","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"4f424610f68c79e4a9ca5261c0d42b892544fb59","datavalue":{"value":"https://doi.org/10.1007/bf02943366","type":"string"},"datatype":"url"},"type":"statement","id":"Q1262115$58BC35F8-7C75-418B-88CF-5056E0F69D1E","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"493a44433c17b49d11434686a071db310984d1d3","datavalue":{"value":"W2089717591","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1262115$D9759087-DF65-45D1-8D1D-876CE886736F","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"970a2cbd0df9c98910950a1062d42b2fee2a74e9","datavalue":{"value":{"entity-type":"item","numeric-id":1078551,"id":"Q1078551"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3c6342113a535c63e3c82f23df49450a08456b41","datavalue":{"value":{"amount":"+0.7540006041526794","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":"Q1262115$967D351F-7BB5-4E12-80D5-E96CE968D32E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"716f49eb4c283491d1ab70885d8fa43cd09d9715","datavalue":{"value":{"entity-type":"item","numeric-id":3982087,"id":"Q3982087"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c10f07f2b6035ae4385c17aff2111fb01e702e36","datavalue":{"value":{"amount":"+0.741656482219696","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":"Q1262115$2BD7BE0F-E1FB-4D75-9388-722BF57C8AB1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"acaaea0cc3fa6a8d30716da35caf95fad192a27c","datavalue":{"value":{"entity-type":"item","numeric-id":1329196,"id":"Q1329196"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e15d2cc7b7a8392d1eb8294011acfb88272db7f6","datavalue":{"value":{"amount":"+0.7403361797332764","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":"Q1262115$1989972D-E0BF-49ED-8742-80ECC8783580","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"59267f35c650dafe313c4eaee81b2b550188f4c2","datavalue":{"value":{"entity-type":"item","numeric-id":4312477,"id":"Q4312477"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"3813f454e19288c92e9d348e5c288de30c6b6fe3","datavalue":{"value":{"amount":"+0.7401277422904968","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":"Q1262115$B1D114C1-D2B0-4663-AD82-F496F4E6B4F9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"038e991c90958baff72363c673bac96b27a2c3c9","datavalue":{"value":{"entity-type":"item","numeric-id":3698284,"id":"Q3698284"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"da74d3a1489f66bb3db0bf29746fd72b850d9af4","datavalue":{"value":{"amount":"+0.7398226261138916","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":"Q1262115$9834F895-4084-41F8-9F00-477C2A8E290B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"A proof rule for while loop in VDM","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/A_proof_rule_for_while_loop_in_VDM"}}}}}