Quelle top_refinement_relations.pvs Sprache: PVS

top_refinement_relations: THEORY
%------------------------------------------------------------------------------
%
% Theories, proofs and test:
% Relation between domain partitioned with equivalence relation,
% codomain partitioned with equivalence relation and two functions:
% f [domain -> codomain] and g [codomain -> domain]
%
%  Author:  Dragan Stosic
%
% In this work I have presented an approach ( aka abstract-algorithm
% formal description ) how to obtain the transformation-relation based
% on equivalence relations on domain and codomain and two functions: one
% from domain to codomain and another from codomain to domain.  I named
% this relation "refinement relation" from the following reason:

% Short description:

% Lets have two equivalence relations: le_T (on domain) and le_U (on
% codomain) and two functions f [ domain - codomain ] and g[ codomain -
% domain ].  If we pick an element t1 from the domain such that le_T(
% t1, g(u1)) then f(t1) belongs to le_U(u2,f(t1)). According to the
% properties of the equivalence relation instead of using f(t1) element
% of the function f-image in some other calculus , we can substitute
% that element with any other which belongs to the Equivalence Class
% derived from the f(t1) element. In other words, we can refine f(t1)
% with the class representative of the Equivalence Class(f(t1)).  We can
% state : f(t1) refined with rep( EquivClass(f(t1)) ->
% RR{(,)(,)...(t1,f(t1)),(t1,rep( EquivClass(f(t1))), (,)...}.

% In other words: t1 can be either paired with the f(t1) or any element
% that satisfied rep( EquivClass(f(t1))).

% The same concept holds in the opposite direction: from codomain to
% domain.

% Note that : My intention is not to dive deep in the rewriting theory
% and to explore equivalence relation as reduction. This work is not
% related to the rewriting equivalence theory; this is refinement
% between elements of collection within the equivalence class induced by
% equivalence relation.

% I have developed two different ways how to formalise the "refinement"
% relation.  First approach is based on extended equivalence relation
% while second approach is based on extended equivalence relation
% induced by the inverse image of the equivalences relations
% respectivelly ( f induces inverse image of le_U and g induces inverse
% imagde of le_T ). Also I have established connection between those two
% definitions of the refinement relations.

% Finally, I have tested my conclusions through several simplest
% examples theories.
%------------------------------------------------------------------------------
BEGIN

  IMPORTING relation_extension,
            relation_extension_props,
            relation_inverse_image,
            relation_inverse_extension,
            rr_rel,
            simplest_examples

END top_refinement_relations

quality94%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.