informalsystems / themis-tracer

A tool for managing complex contexts for developing critical systems
Apache License 2.0
4 stars 0 forks source link

Must support "views" #29

Open shonfeder opened 3 years ago

shonfeder commented 3 years ago

A view gives a perspective on things.

As Joseph noted in a meeting, we need different docs for different audiences.

Viewpoint modeling

In RM-ODP modeling See Viewpoints Modeling

The concept of RM-ODP viewpoints framework, therefore, is to provide separate viewpoints into the specification of a given complex system. These viewpoints each satisfy an audience with interest in a particular set of aspects of the system. Associated with each viewpoint is a viewpoint language that optimizes the vocabulary and presentation for the audience of that viewpoint.

In terms of algebraic semiotics, a viewpoint model is just a mapping from the common system onto a reference system common to a subset of the stakeholders.

Implementation view

See http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16.7656&rep=rep1&type=pdf

Views are used to bind actual (values in) modules to generic module itnerfaces (i.e., theory modules), in order to instantiate generics. Because modules may involve information hiding, views only assert the behavioral satisfaction of the axioms in their source theory by the target module). However, proving that such axioms are satisfied should not necessarily be part of a system intended to be practical for ordinary use. … views are used for recording a programmer’s belief that the axioms in the source theory hold in the target module. Support for such a belief may be provided off line on the back of an envelope, by giving a formal mechanical proof, or by anything between these extremes; the belief may even be left unsupported, although this is not recommended. The nature of the support given (e.g., a scanned image of the envelope back, or the source file of the machine proof) can be stored with the view in the module graph.