A Method to Deduce and Synthesize the Dafny Programs

We propose a systematic method to deduce and synthesize the Dafny programs. First, the specification of problem is described in strict mathematical language. Then, the derivation process uses program specification transformation technology to perform equivalent transformation. Furthermore, Dafny program is synthesized through the obtained recursive relationship and loop invariants. Finally, the functional correctness of Dafny program is automatically verified by Dafny verifier or online tool. Through this method, we deduce and synthesize Dafny programs for many typical problems such as the cube sum problem, the minimum (or maximum) contiguous subarray problems, several searching problems, several sorting problems, and so on. Due to space limitation, we only illustrate the development process of Dafny programs for two typical problems: the minimum contiguous subarray problem and the new local bubble sorting problem. It proves that our method can effectively improve the correctness and reliability of Dafny program developed. What’s more, we demonstrate the potential of the deductive synthesis method by developing a new local bubble Sorting program.

Download Full-text

Inverse sorting problem by minimizing the total weighted number of changes and partial inverse sorting problems

Computational Optimization and Applications ◽

10.1007/s10589-006-0394-6 ◽

2006 ◽

Vol 36 (1) ◽

pp. 55-66 ◽

Cited By ~ 14

Author(s):

X. G. Yang ◽

J. Z. Zhang

Keyword(s):

Sorting Problem ◽

Partial Inverse ◽

Sorting Problems ◽

Weighted Number

Download Full-text

Method of Multilevel Adaptive Synthesis of Monitoring Object Knowledge Graphs

Applied Sciences ◽

10.3390/app11146251 ◽

2021 ◽

Vol 11 (14) ◽

pp. 6251

Author(s):

Kirill Krinkin ◽

Alexander Vodyaho ◽

Igor Kulikov ◽

Nataly Zhukova

Keyword(s):

Complexity Analysis ◽

Synthesis Method ◽

Telecommunication Networks ◽

Synthesis Methods ◽

Complex Objects ◽

Object Knowledge ◽

Deductive Synthesis ◽

Knowledge Graphs ◽

State Models ◽

Object Models

The paper introduces a method for adaptive deductive synthesis of state models, of complex objects, with multilevel variable structures. The method makes it possible to predict the state of objects using the data coming from them. The data from the objects are collected with sensors installed on them. Multilevel knowledge graphs (KG) are used to describe the observed objects. The new adaptive synthesis method develops previously proposed inductive and deductive synthesis methods, allowing the context to be taken into account when predicting the states of the monitored objects based on the data obtained from them. The article proposes the algorithm for the suggested method and presents its computational complexity analysis. The software system, based on the proposed method, and the algorithm for multilevel adaptive synthesis of the object models developed, are described in the article. The effectiveness of the proposed method is shown in the results from modeling the states of telecommunication networks of cable television operators.

Download Full-text

Boundary Variable Precision Dominance-Based Rough Set Approach in Multicriteria Sorting Problems

Advanced Materials Research ◽

10.4028/www.scientific.net/amr.734-737.3102 ◽

2013 ◽

Vol 734-737 ◽

pp. 3102-3106

Author(s):

Hong Li ◽

Guo Yin Wang ◽

Guang Lei Gou ◽

Wen Liu

Keyword(s):

Rough Set ◽

Classification Problems ◽

Empirical Results ◽

Variable Precision ◽

Sorting Problem ◽

Decision Attributes ◽

Sorting Problems ◽

Novel Method ◽

Multicriteria Sorting ◽

Preference Orders

This paper provides a novel method of boundary variable precision dominance-based rough set approach (BVP-DRSA) to solve multicriteria sorting problem that differs from usual classification problems since it takes into account preference orders in the description of objects by condition and decision attributes. The major contribution of our BVP-DRSA method is that it combines variable precision and dominance-based rough set approach (DRSA). This approach is different from the dominance-based rough set approach (DRSA) because it takes boundary into account and can deal with boundary directly. Comparative experiments form datasets of UCI and empirical results shows that our BVP-DRSA is far more efficient than directly using already known classing algorithms and DRSA.

Download Full-text

Deductive Synthesis of Algorithms in Human-Computer Interaction

Applied Mechanics and Materials ◽

10.4028/www.scientific.net/amm.610.312 ◽

2014 ◽

Vol 610 ◽

pp. 312-315

Author(s):

Hai He Shi ◽

Hai Peng Shi

Keyword(s):

Software Development ◽

Human Computer Interaction ◽

Algorithm Design ◽

Synthesis Method ◽

Program Synthesis ◽

Selection Problem ◽

Deductive Synthesis ◽

Formal Problem ◽

Proof Of Correctness ◽

Computer Interaction

Deductive synthesis is a method of software development where an algorithm is derived from a formal problem specification which guarantees the reliability of final product. The paper introduces a program synthesis method PAR most of whose synthesis steps are mechanical and some of them can be done interactively by human-computer interaction, and formally synthesizes a dependable algorithm for a selection problem supported by PAR method and PAR platform. Program synthesis based on PAR covers a number of classical algorithm design tactics, develops algorithmic programs together with their proof of correctness, and makes the algorithm more reliable and solving idea more understandable.

Download Full-text

Deductive Synthesis of Networks Hierarchical Knowledge Graphs

International Journal of Embedded and Real-Time Communication Systems ◽

10.4018/ijertcs.2021070103 ◽

2021 ◽

Vol 12 (3) ◽

pp. 32-48

Author(s):

Kirill Krinkin ◽

Alexander Ivanovich Vodyaho ◽

Igor Kulikov ◽

Nataly Zhukova

Keyword(s):

Hierarchical Structure ◽

Real World ◽

Synthesis Method ◽

Low Complexity ◽

Graph Models ◽

Telecommunications Networks ◽

Heterogeneous Objects ◽

Deductive Synthesis ◽

Knowledge Graphs ◽

Computational Resources

The article focuses on developing of a deductive synthesis method for building telecommunications networks (TN) hierarchical knowledge graphs (KG). Synthesized KGs can be used to solve search, analytical, and recommendation (forecast) problems. TNs are complex heterogeneous objects. The synthesis of knowledge graphs of such objects requires much computational resources. The proposed method provides a low complexity of the synthesis of KG of TN by taking into account their hierarchical structure. The authors propose to do synthesis by direct downward multilevel inference and reverse multilevel inference. The article analyses existing graph models of TNs and methods for their building. Detailed description of the proposed method of networks hierarchical KGs synthesis is given. In order to evaluate the deductive synthesis method, a prototype of the system is developed. The provided real-world example shows how telecommunications networks hierarchical knowledge graphs are synthesized and used in practice. Finally, conclusions are formulated, and the areas of further research are identified.

Download Full-text

A Novel Multi-Criteria Decision Sorting Approach based on Chebyshev's Theorem for Supplier Classification Problem

Engineering and Scientific International Journal ◽

10.30726/esij/v8.i2.2021.82012 ◽

2021 ◽

Vol 8 (2) ◽

Author(s):

Mohammad Azadfallah

Keyword(s):

Decision Making ◽

Classification Problem ◽

Multiple Attribute Decision Making ◽

Decision Problems ◽

Ranking Problem ◽

Sorting Problem ◽

Multiple Attribute ◽

Electre Tri ◽

Sorting Problems ◽

Ranking Problems

One of the interesting features of Multi-Criteria Decision Making/ Multiple Attribute Decision Making (MCDM/ MADM) is that a number of techniques that can be used to solve the same problem. In general, three common categories of decision problems are choice problem, ranking problem, and sorting problem. While, the issue of choice and ranking problems is more emphasized in MCDM/ MADM, but the literature weakly consider sorting problems. Several solutions for the above problem are suggested (i.e., Flow sort, AHP-Sort, ELECTRE Tri, etc.). Theoretically, there is no reason to be limited to these techniques. Hence, in this paper we propose a novel multi-criteria sorting method that is based on Chebyshev’s theorem. More specifically, different from other studies on MCDM sorting problems, which put more emphasis on the extension of new models, this work attempts to present a general framework using the Chebyshev’s inequality, to transform the results of conventional MCDM models from ranking format to sort mode. Finally, the proposed approach is compared with three existed models. Compared results show that the proposed method is efficient and the results are stable.

Download Full-text

Sentence-Based Experience Logging in New Hearing Aid Users

American Journal of Audiology ◽

10.1044/2020_aja-19-00077 ◽

2020 ◽

Vol 29 (3S) ◽

pp. 631-637

Author(s):

Katja Lund ◽

Rodrigo Ordoñez ◽

Jens Bo Nielsen ◽

Dorte Hammershøi

Keyword(s):

Hearing Aid ◽

Patient Experiences ◽

Online Tool ◽

Rehabilitation Process ◽

Hearing Rehabilitation ◽

Clinical Observations ◽

Hearing Aid Use ◽

Wide Range ◽

Insight Into ◽

Shed Light

Purpose The aim of this study was to develop a tool to gain insight into the daily experiences of new hearing aid users and to shed light on aspects of aided performance that may not be unveiled through standard questionnaires. Method The tool is developed based on clinical observations, patient experiences, expert involvement, and existing validated hearing rehabilitation questionnaires. Results An online tool for collecting data related to hearing aid use was developed. The tool is based on 453 prefabricated sentences representing experiences within 13 categories related to hearing aid use. Conclusions The tool has the potential to reflect a wide range of individual experiences with hearing aid use, including auditory and nonauditory aspects. These experiences may hold important knowledge for both the patient and the professional in the hearing rehabilitation process.

Download Full-text