[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Doubt about refinement
Reading the paper , I ended up with some doubts about the refinement:
Allocator => SimpleAllocator
I understand that refinement is an implication, in the sense that SchedulingAllocator satisfies the SimpleAllocator's spec as well. I got into trouble trying to understand the module AllocatorRefinement, which is stated below:
Simple == INSTANCE SimpleAllocator
SimpleAllocator == Simple!SimpleAllocator
THEOREM Allocator => SimpleAllocator
Actually, I can't understand what this means: Simple!SimpleAllocator (the use of operator "!" is not clear to me). I tried to read about it in Specifying Systems, but the question still remains.
Furthermore, what should be the conditions to write a spec that implements another one? Thanks!
Pedro Yuri Arbs Paiva
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129