{"entities":{"Q689297":{"pageid":691146,"ns":120,"title":"Item:Q689297","lastrevid":63499263,"modified":"2026-04-11T13:34:32Z","type":"item","id":"Q689297","labels":{"en":{"language":"en","value":"``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 445060"}},"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":"Q689297$0786114A-AAA9-4FB5-95E4-50FD5547FD53","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"14e01fb19417b731adeb0691e62b6beb202ac753","datavalue":{"value":{"text":"``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q689297$76E2CDE5-3CC6-46C8-ADC6-685406A1DE6D","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"3fe1d8f52aba42a83f04defed3af0e938e359783","datavalue":{"value":"0788.68094","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689297$F35A37B2-4CC8-482F-BA9C-B1B81F24CD03","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"e17edc3e5684fdeb77b6c95ee6d0369a39db5b9e","datavalue":{"value":"10.1016/0304-3975(93)90248-R","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689297$83880D23-16D6-4E38-92AC-CE68DB11904C","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"f3c424cd94a60f9664f9fb69cc6027e75cc7ff3f","datavalue":{"value":{"entity-type":"item","numeric-id":123643,"id":"Q123643"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$63815A22-52AB-4A7C-B05F-D7FF0A76C0BE","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"61a335d09cf4057e5c760f9e6e170367a29098e7","datavalue":{"value":{"time":"+1994-06-02T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q689297$1D8816CE-AC09-4416-BF5F-AAEDABAEF05B","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"53d42d5b3fca4ad1e21b3b94fcefba1f6395b115","datavalue":{"value":"The paper generalizes Burstall's (and that of Manna and Waldinger) intermittent assertions method to handle some properties of nondeterministic and parallel programs. Thus, as in operational semantics of programming languages, programs are modeled by transition systems, and program execution by complete traces. Termination and total correctness are modeled by inevitability properties, which are proved by Burstall's method and by some more abstract induction principles which generalise Burstall's method.   The soundness, completeness and semantic completeness of this induction principle is proved.   As the authors say, this study should be extended so as to take fairness hypotheses for parallel programs into account, and in order to obtain better presentations for logic programming.","type":"string"},"datatype":"string"},"type":"statement","id":"Q689297$C339EC1E-590F-45A1-8568-0D0AE59CAD57","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"850715937341d072522c2b6dfe4fd00f3d07e86f","datavalue":{"value":{"entity-type":"item","numeric-id":689296,"id":"Q689296"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$3FC36200-5F7B-45D2-B66D-12C2A4C080AD","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"7cfff2e3b7f009b69ae82e4aa296ae1902bd02ff","datavalue":{"value":"68Q60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689297$7C886FF8-A2CD-4CC6-94B8-798F23C2EAC3","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"0ab3b15f7f3053fda242d92da72e80fc28a81616","datavalue":{"value":"445060","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q689297$460113DB-38C8-4FB2-85BE-D2DBA428FCE4","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"5e381b994a9c0ce3eb69287257f5288ebf06f2b7","datavalue":{"value":"nondeterministic programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q689297$5CD2F9B0-0DA0-429F-8688-726E952CD8E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"855af08d63de68a214880a14dc080a2a72230738","datavalue":{"value":"parallel programs","type":"string"},"datatype":"string"},"type":"statement","id":"Q689297$EC8C843A-8C35-4670-AACF-3990C8371102","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"6d9c2e1f00facc619242af9af43a4aae006f38ad","datavalue":{"value":"transition systems","type":"string"},"datatype":"string"},"type":"statement","id":"Q689297$2F3EFEE8-7215-43F8-B74B-53349F8199E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"ca349b7534ee4c6daef46219f1870f6141cd3cfb","datavalue":{"value":"induction principles","type":"string"},"datatype":"string"},"type":"statement","id":"Q689297$27F58990-DD87-4024-9EFC-A6046279912B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"05ea7bb225dfc0f1ba88b53ac8e959b98d283c0d","datavalue":{"value":"semantic completeness","type":"string"},"datatype":"string"},"type":"statement","id":"Q689297$FDE7B869-12B9-4615-97D6-11A445ACB17D","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"66475c89deaa1b82e2a733011ec9769bb2327168","datavalue":{"value":{"entity-type":"item","numeric-id":655408,"id":"Q655408"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$EB4794E3-CE92-46C7-8BA2-848D2F918193","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"aabe6d988e05fe3a7b00666b4b0ee76e06b180c4","datavalue":{"value":{"entity-type":"item","numeric-id":655409,"id":"Q655409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$9778178A-412A-4B7C-899B-4772207D70EB","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":"Q689297$CD8E7003-B62A-474D-9498-CB99FCA11FF5","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"f98fcb838e1ffda9760ba9520630c9b15bdc35b0","datavalue":{"value":{"entity-type":"item","numeric-id":3673097,"id":"Q3673097"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$64EF0C10-4A70-4377-ACA6-5A2B7F666D7B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b2204ee7d30bcfa8fbee857183801f78bafc2ef2","datavalue":{"value":{"entity-type":"item","numeric-id":3763571,"id":"Q3763571"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$F3A965CB-C8A3-4B2C-8D6B-E759DC0B5511","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2d346d8485da0bc889f787fa277d331b616d4df2","datavalue":{"value":{"entity-type":"item","numeric-id":4054648,"id":"Q4054648"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$5205BADD-8633-41AF-AEC6-A90DCFF115D3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1dcaba85eaf9b02283987ee8f5ec2f8f6402ce65","datavalue":{"value":{"entity-type":"item","numeric-id":689297,"id":"Q689297"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$C5FD3B3E-5B7E-4DD6-92E5-97DCB2E8755B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5ab828076764dd3c1c3bcd0118a6663e784bb9b","datavalue":{"value":{"entity-type":"item","numeric-id":1071491,"id":"Q1071491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$BA245ABA-D4A3-48D3-BE7E-721B25C07876","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a9143b9caec2c35ed69b6720f87afb357eeeb92","datavalue":{"value":{"entity-type":"item","numeric-id":3962450,"id":"Q3962450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$DE91432A-C5D4-484E-A94B-1150759BC4AB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6130a72bad290e99b4d30823cf592f64ef05b4a8","datavalue":{"value":{"entity-type":"item","numeric-id":5584402,"id":"Q5584402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$F0637095-7C51-4A90-A6D5-07F7738CEF7E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5710cd0fb8b5907d40eeada6e14d4018e26669a5","datavalue":{"value":{"entity-type":"item","numeric-id":1255942,"id":"Q1255942"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$2F841390-058D-4265-B06A-868BF664BA65","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7e09f7681257b92526d42b556170b42e07509410","datavalue":{"value":{"entity-type":"item","numeric-id":4745241,"id":"Q4745241"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$EFD992DD-A0EB-4FE3-9563-0C154196773B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"56485b9a4814bcf88c5da509c43cc487af1d7b47","datavalue":{"value":{"entity-type":"item","numeric-id":4144164,"id":"Q4144164"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$AEBE7A88-5D16-482D-82DD-C4F1B3EC9B23","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2c6d7fcad26f92b9f45640be0a452cceb831f5e2","datavalue":{"value":{"entity-type":"item","numeric-id":4136512,"id":"Q4136512"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q689297$DC1BCB1A-D601-446A-B4E5-8C0360440DFF","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a631b3e44b2e12cffd8107e92668daf95a6850c1","datavalue":{"value":{"entity-type":"item","numeric-id":3802590,"id":"Q3802590"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"01b99e1cfccd5bb8231a21673048c213cb8253d2","datavalue":{"value":{"amount":"+0.9147733","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":"Q689297$480668DE-5C04-418E-B8F9-7725025D92C7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0c42abca5f1957af99c29414df960c3ba393d8e3","datavalue":{"value":{"entity-type":"item","numeric-id":1071491,"id":"Q1071491"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"77e7a95072e113813f0f06be8469bfe8228db218","datavalue":{"value":{"amount":"+0.8697836","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":"Q689297$3D7E79C5-A11F-4C3C-9D67-92D4A066B0B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e6d3a255266f36191915db130af5af18c5f18eb5","datavalue":{"value":{"entity-type":"item","numeric-id":1271855,"id":"Q1271855"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e0b33f557a2440e67805e33dfecbf566eb11a7b4","datavalue":{"value":{"amount":"+0.8420906","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":"Q689297$33D6DA29-72AB-4B1B-846E-365CCB5FF182","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"714e15e5a2ba4fff06e9121fed38d3236869a4fd","datavalue":{"value":{"entity-type":"item","numeric-id":1267035,"id":"Q1267035"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"0274bc437db33ebbf865cde7e67cda415497446f","datavalue":{"value":{"amount":"+0.8416915","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":"Q689297$39BF1655-28FF-4598-8D80-80D6E3F1AD71","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"12a36762cfa69c12d80d136d8153172ea3193b7b","datavalue":{"value":{"entity-type":"item","numeric-id":5097622,"id":"Q5097622"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"78895f40e7da50ba91341e3c9a487207f567492a","datavalue":{"value":{"amount":"+0.83729535","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":"Q689297$29073E23-9A27-43B4-8468-A8E8832DC49F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed58649527b45a30c8bf0f209a9b2229e7451a53","datavalue":{"value":{"entity-type":"item","numeric-id":1267030,"id":"Q1267030"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"d608e3b7127e112e9566f1719a0e04ea8feab7c2","datavalue":{"value":{"amount":"+0.83320117","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":"Q689297$ABB6C477-11BC-4D56-875E-2840007A7539","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b9968a81f101b3dda94d0e82c4e51378c913a3db","datavalue":{"value":{"entity-type":"item","numeric-id":3341880,"id":"Q3341880"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ab02b694b1893ef6301c8c1f08d9f2d0fa3799ac","datavalue":{"value":{"amount":"+0.8325513","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":"Q689297$0E55CFC9-B34B-42AA-80E0-DC7A05860040","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"8266f2c8ef040bdae8a8d17dbab7410a4f0f3244","datavalue":{"value":{"entity-type":"item","numeric-id":4923368,"id":"Q4923368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"e6c609bacedbfd3b76938f39d26f02f6a63a3428","datavalue":{"value":{"amount":"+0.8324864","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":"Q689297$B55A4FBB-5F22-45D5-84C7-214C30AF522C","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/%60%60A_la_Burstall%27%27_intermittent_assertions_induction_principles_for_proving_inevitability_properties_of_programs"}}}}}