.nr PS 11
.nr VS 14
.so roff.defs
.nr P 1 Presentation Flag
.nr D 0 Document Flag
.LP
.TL
BSI VDM-SL Type Model and Proof Theory
.AU
Roger Bishop Jones
.AI
ICL Defence Systems
.AB
.ct D
gggg
.cx
.ct P
This document consists of overheads for introducing the discussion
of the VDM panel (technical subgroup) on the above topic.
.cx
.AE
.ds LH \s-8VDM-SL Type Model\s+8
.ds CH \s-2\s+2
.ds RH \s-8\1988-03-04\s+8
.ds LF \s-8DTC/RBJ/094\s+8
.ds CF \s-2\s+2
.ds RF \s-8Issue 0.1 Page \\n(PN\s+8
.ct P
.nr PS 20
.nr VS 24
.cx
.KS
.NH
SOME RELEVANT DOCUMENTS
.DS L


A Type Model for VDM - Brian Monahan 


Notes on VDM Type Model - Roger Jones


Kentrikos - Havelund & Wagner


Notes on Kentrikos - Roger Jones


Plan for VDM-SL Proof Theory - Roger Jones


Naive Denotational Semantics - Blikle & Tarleki


A Semantics of Multiple Inheritance - Cardelli


UST in SML, LPF in SML - Roger Jones 
.DE
.KE
.KS
.NH
PRIMARY ISSUES (from proof-theoretic viewpoint)
.DS C



REFLEXIVE DOMAINS



TYPE INHERITANCE



FUNCTIONS SPACES
(continuity, strictness)



STRATIFICATION
(1, 2 or 3 layers)


When do we need to have these issues settled?
.DE
.KE
.KS
.NH
DIFFICULTIES WITH BQM MODEL
.DS C
Is it 2 or 3 layers?
(and why)

How does the record type constructor work
(proof of closure please)

Quantification and Continuity 
.DE
.KE
.KS
.NH
CONTINUITY
.DS C
Identifying FORMULAE with
CONTINUOUS BOOLEAN EXPRESSIONS
gives a logic with
NEGLIGIBLE expressive power.

QUANTIFICATION is NOT CONTINUOUS.

IMPLICTION is NOT MONOTONIC (or strict).

In the VDM RL semantics, specifications
which ought to denote discontinuous functions
simply fail to have models, they are inconsistent.
.DE
.KE
.KS
.NH
WHAT FUNCTION SPACE IS BEST?
.DS C

SCOTT CONTINUOUS?
No, continuity is too strong a constraint.
(for a specification language)


BLIKLE/Z PARTIAL FUNCTION SPACE.
(A pf B) = A \*(be B = {r | r\(ib \*m(A \(mu B) \*e r is many-one}
No, strictness is too strong a constraint.


KENTRIKOS PARTIAL FUNCTION SPACE
No, it doesn't admit closure.
(a little overpopulated)


ADD BOTTOMS and use TOTAL FUNCTIONS?
(A pf B) = (A+?)\(->(B+?)


RBJ PF SPACE?
(A pf B) = (A + \(es) \*(be (B - \(es)
.DE
.KE
.nr PS 14
.nr VS 20
.nr PS 20
.nr VS 24
.KE