{"entities":{"Q7361195":{"pageid":31519124,"ns":120,"title":"Item:Q7361195","lastrevid":105363779,"modified":"2026-10-07T13:35:03Z","type":"item","id":"Q7361195","labels":{"en":{"language":"en","value":"Pop-Refinement"}},"descriptions":{"en":{"language":"en","value":"AFP entry Pop_Refinement"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"e235089340e505f656e0b4be82142f3343800739","datavalue":{"value":"https://isa-afp.org/entries/Pop_Refinement.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361195$5AA9A182-0221-4C60-BC6D-C89EA5E18474","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"5db05d28484b9b27c9ad59c82fa62df63d966b30","datavalue":{"value":{"time":"+2014-07-03T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361195$B6EF665C-BEF8-42A6-9902-F26F1F4688D2","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"3a57a8053a2444e0b242d4e145126ab68e2bedf1","datavalue":{"value":"Alessandro Coglio","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361195$B1C99085-7B1B-4FEB-BB3C-4F42B49FB77F","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"58d8d10482c174313443405c0db785e670a62d66","datavalue":{"value":{"text":"Pop-Refinement","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361195$2158FF2F-3D3E-41F9-9FDC-4C5655F79A0E","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"14c59919e8b57cede7e1913ccddcb4d5469c3a9a","datavalue":{"value":"Pop-refinement is an approach to stepwise refinement, carried out inside an interactive theorem prover by constructing a monotonically decreasing sequence of predicates over deeply embedded target programs. The sequence starts with a predicate that characterizes the possible implementations, and ends with a predicate that characterizes a unique program in explicit syntactic form. Pop-refinement enables more requirements (e.g. program-level and non-functional) to be captured in the initial specification and preserved through refinement. Security requirements expressed as hyperproperties (i.e. predicates over sets of traces) are always preserved by pop-refinement, unlike the popular notion of refinement as trace set inclusion. Two simple examples in Isabelle/HOL are presented, featuring program-level requirements, non-functional requirements, and hyperproperties.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361195$E68AAB47-40CA-4B64-8A93-081041908F14","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"b5d5978f4bdf14ef5fd8b71ce390dbec5034a1e6","datavalue":{"value":{"entity-type":"item","numeric-id":805251,"id":"Q805251"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$D6CE2D6E-3E8E-41E0-A82B-EAFD95C2D475","rank":"normal"},{"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":"Q7361195$FD5F4851-7D00-4668-A83E-F02A44B6115D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c7f815bf2ad909de0fa6e89988501157b6f777d2","datavalue":{"value":{"entity-type":"item","numeric-id":5554728,"id":"Q5554728"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$C79DA939-B749-4F6A-AF48-2C5BAFAA10BB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"db463348657cf41d5ff4d422c54e0c686e6e5dfc","datavalue":{"value":{"entity-type":"item","numeric-id":2554952,"id":"Q2554952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$70897812-0BD1-4995-A8A3-531B85342500","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d2d1dad5172901081e5c4e849118356615b18a74","datavalue":{"value":{"entity-type":"item","numeric-id":4934624,"id":"Q4934624"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$06DF5DF9-116A-4061-B0D6-53CEEDD2A4B9","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":"Q7361195$4ACDD4F5-018A-4B21-A630-ECA45E581385","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"78b7dee6e7d17cf76652241ef534151263d94379","datavalue":{"value":{"entity-type":"item","numeric-id":5617313,"id":"Q5617313"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$89C235D5-5203-4160-BA17-59E400C6C5C6","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$AED8F84F-4E18-4B18-BC52-7F965970476F","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"74073bb97e06ee9cb8d0a44748848fdf77fe551f","datavalue":{"value":{"entity-type":"item","numeric-id":7360798,"id":"Q7360798"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$A5EC06E3-D81A-4CBA-8649-CB20BD760690","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361195$8E5EB06A-905F-457A-8D49-B78224F71756","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Pop-Refinement","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Pop-Refinement"}}}}}