From 584eac7027cd4d29c5ca8744453ffeea8f18b501 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 7 Jun 2015 09:25:53 +0200 Subject: Represent external worlds by a coinductive type rather than an inductive type. As noticed by R. Krebbers, an inductive type for external worlds implies that all sequences of program-world interactions are finite, which is not the case. --- common/Determinism.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common/Determinism.v') diff --git a/common/Determinism.v b/common/Determinism.v index d0099ba9..7ea19663 100644 --- a/common/Determinism.v +++ b/common/Determinism.v @@ -36,7 +36,7 @@ Require Import Behaviors. that this external call succeeds, has result [r], and changes the world to [w]. *) -Inductive world: Type := +CoInductive world: Type := World (io: ident -> list eventval -> option (eventval * world)) (vload: memory_chunk -> ident -> int -> option (eventval * world)) (vstore: memory_chunk -> ident -> int -> eventval -> option world). -- cgit