Wyniki wyszukiwania - BazTech

1

ChR: Dynamic Functional Constraints Checking in R

Grzanek K.

Journal of Applied Computer Science Methods

|

2017

|

Vol. 9 No. 1

65--78

EN

Dynamic typing of R programming language may issue some quality problems in large scale data-science and machine-learning projects for which the language is used. Following our efforts on providing gradual typing library for Clojure we come with a package chR - a library that offers functionality of run-time type-related checks in R. The solution is not only a dynamic type checker, it also helps to systematize thinking about types in the language, at the same time offering high expressivenes and full adherence to functional programming style.

2

Low-Cost Dynamic Constraint Checking for the JVM

Grzanek K.

Journal of Applied Computer Science Methods

|

2016

|

Vol. 8 No. 2

115--136

EN

Using formal methods for software verification slowly becomes a standard in the industry. Overall it is a good idea to integrate as many checks as possible with the programming language. This is a major cause of the apparent success of strong typing in software, either performed on the compile time or dynamically, on runtime. Unfortunately, only some of the properties of software may be expressed in the type system of event the most sophisticated programming languages. Many of them must be performed dynamically. This paper presents a flexible library for the dynamically typed, functional programming language running in the JVM environment. This library offers its users a close to zero run-time overhead and strong mathematical background in category theory.

3

Pattern-based Rewriting through Abstraction

Bottoni P., Guerra E., de Lara J.

Fundamenta Informaticae

|

2016

|

Vol. 144, nr 2

109--160

EN

Model-based development relies on models in different phases for different purposes, with modelling patterns being used to document and gather knowledge about good practices in specific domains, to analyse the quality of existing designs, and to guide the construction and refactoring of models. Providing a formal basis for the use of patterns would also support their integration with existing approaches to model transformation. To this end, we turn to the commonly used, in this context, machinery of graph transformations and provide an algebraic-categorical formalization of modelling patterns, which can express variability and required/forbidden application contexts. This allows the definition of transformation rules having patterns in left and right-hand sides, which can be used to express refactorings towards patterns, change the use of one pattern by a different one, or switch between pattern variants. A key element in our proposal is the use of operations to abstract models into patterns, so that they can be manipulated by pattern rules, thus leading to a rewriting mechanism for classes of graphs described by patterns and not just individual graphs. The proposal is illustrated with examples in object-oriented software design patterns and enterprise architecture patterns, but can be applied to any other domain where patterns are used for modelling.

4

An Algebraic Semantics for QVT-Relations Check-only Transformations

Guerra E., de Lara J.

Fundamenta Informaticae

|

2012

|

Vol. 114, nr 1

73-101

EN

QVT is the standard for model transformation defined by the OMG in the context of the Model-Driven Architecture. It is made of several transformation languages. Among them, QVTRelations is the one with the highest level of abstraction, as it permits developing bidirectional transformations in a declarative, relational style. Unfortunately, the standard only provides a semiformal description of its semantics, which hinders analysis and has given rise to ambiguities in existing tool implementations. In order to improve this situation, we propose a formal, algebraic semantics for QVT-Relations check-only transformations, defining a notion of satisfaction of QVT-Relations specifications by models.

5

Adhesivity with Partial Maps instead of Spans

Heindel T.

Fundamenta Informaticae

|

2012

|

Vol. 118, nr 1-2

1-33

EN

The introduction of adhesive categories revived interest in the study of properties of pushouts with respect to pullbacks that started over thirty years ago for the category of graphs. Adhesive categories - of which graphs are the 'archetypal' example - are defined by a single property of pushouts along monos that implies essential lemmas and central theorems of double pushout rewriting such as the local Church-Rosser Theorem. The present paper shows that a strictly weaker condition on pushouts suffices to obtain essentially the same results: it suffices to require pushouts to be hereditary, i.e. they have to remain pushouts when they are embedded into the associated category of partial maps. This fact however is not the only reason to introduce partial map adhesive categories as categories with pushouts along monos (of a certain stable class) that are hereditary. There are two equally important motivations: first, there is an application relevant example category that cannot be captured by the more established variations of adhesive categories; second, partial map adhesive categories are 'conceptually similar' to adhesive categories as the latter can be characterized as those categories with pushout along monos that remain bi-pushouts when they are embedded into the associated bi-category of spans. Thus, adhesivity with partial maps instead of spans appears to be a natural candidate for a general rewriting framework.

6

Timed Delay Bisimulation is an Equivalence Relation for Timed Transition Systems

Gribovskaya N., Virbitskaite I.

Fundamenta Informaticae

|

2009

|

Vol. 93, nr 1-3

127-142

EN

Timed transition systems are a widely studied model for real-time systems. The intention of the paper is to show the applicability of the general categorical framework of openmaps in order to prove that timed delay equivalence is indeed an equivalence relation in the setting of timed transition systems with invariants. In particular, we define a category of the model under consideration and an accompanying (sub)category of observations to which the corresponding notion of open maps is developed. We then use the open maps framework to obtain an abstract equivalence relation which is established to coincide with timed delay bisimulation.

7

Modular Construction of Finite and Complete Prefixes of Petri net Unfoldings

Madalinski A., Fabre E.

Fundamenta Informaticae

|

2009

|

Vol. 95, nr 1

219-244

EN

This paper considers distributed systems, defined as a collection of components interacting through interfaces. Components, interfaces and distributed systems are modeled as Petri nets. It is well known that the unfolding of such a distributed system factorises, in the sense that it can be expressed as the composition of unfoldings of its components. This factorised form of the unfolding generally provides a more compact representation of the system runs, because each component does not need to represent the possible choices (conflicts) appearing in the other components. Moreover, the unfolding factorisation makes it possible to analyse the system by parts. The paper focuses on the derivation of a finite and complete prefix (FCP) in the unfolding of a distributed system. Specifically, one would like to directly obtain such a FCP in factorised form, without computing first a FCP of the global distributed system and then factorising it. The construction of such a “modular FCP” is based on deriving summaries of component behaviours w.r.t. their interfaces, that are then communicated to the neighbouring components. The latter combine these summaries with their local behaviours, and prepare interface summaries for the next components. This globally takes the form of a message passing algorithm, where the global system is never considered.

8

A Categorical View on Algebraic Lattices in Formal Concept Analysis

Hitzler P., Krötzsch M., Zhang G-Q.

Fundamenta Informaticae

|

2006

|

Vol. 74, nr 2,3

301-328

EN

Formal concept analysis has grown from a new branch of the mathematical field of lattice theory to a widely recognized tool in Computer Science and elsewhere. In order to fully benefit from this theory, we believe that it can be enriched with notions such as approximation by computation or representability. The latter are commonly studied in denotational semantics and domain theory and captured most prominently by the notion of algebraicity, e.g. of lattices. In this paper, we explore the notion of algebraicity in formal concept analysis from a category-theoretical perspective. To this end, we build on the notion of approximable concept with a suitable category and show that the latter is equivalent to the category of algebraic lattices. At the same time, the paper provides a relatively comprehensive account of the representation theory of algebraic lattices in the framework of Stone duality, relating well-known structures such as Scott information systems with further formalisms from logic, topology, domains and lattice theory.