Network clustering (graph clustering) plays a crucial role in discovering the inherent structures within networks. MapReduce-based structural clustering algorithm for networks (MRSCANs) designed based on MapReduce's parallel computing model, efficiently handles large-scale data. However, MRSCAN can only be tested through experiments, and its correctness cannot be guaranteed. To address this issue, this article has achieved the first implementation of functional MRSCAN modeling and subjected it to rigorous mechanized verification in Isabelle. First, based on Google's MapReduce model type definition and higher-order generic functions, a general MapReduce-based algorithm functional modeling framework is constructed across the fundamental global phases of Map, Shuffle, and Reduce. Moreover, diverse strategies are devised during the Shuffle phases according to user requirements, enhancing the applicability and generality of the MapReduce functional modeling framework. Second, formalizing the definition of MRSCAN, is delineated into four key steps: similarity calculation, core calculation, dimension expansion, and structural clustering. Furthermore, the MapReduce functional modeling framework is applied to these four steps to achieve the functional modeling of MRSCAN, which improves efficiency compared to other structural clustering algorithm for networks (SCANs) algorithms. Lastly, a verification framework for MapReduce-based algorithms is proposed at both the global and shuffle stages. Based on this framework, the correctness and reliability of MRSCAN are ensured. The model framework and verification framework of MapReduce-based algorithms proposed in this article can not only address functional modeling and verification of MRSCAN but also provide a reference for a series of other MapReduce-based functional program designs and proofs.

When cyber-physical systems (CPSs) are operational, its computing units frequently interact with complex and uncertain physical environments in time and space. To ensure the safety of the system, it is often necessary that the physical entities and information systems of CPS operate in a consistent manner at the temporal and spatial levels. However, most of the existing studies on spatio-temporal consistency modeling and verification of CPS are limited in the ability to deal with uncertainties. To address this issues, in this article, we propose a modeling and verification method for spatio-temporal consistency of CPS in uncertain environments. First, we propose a modeling language (stochastic spatio-temporal modeling language, SSTL) for the spatio-temporal domain of CPS. It can explicitly model the spatio-temporal constraints of CPS as well as deal with the spatio-temporal behavior of accompanying probabilities. Second, we propose a framework for spatio-temporal consistency verification. In the first step of this framework, we propose a worst-case time satisfiability algorithm to verifying the time safety of CPS. In the second step, we develop a prototype tool called “SSTL2NSHA” that is able to convert SSTL into the NHSA model supported by UPPAAL-statistical model checking (UPPAAL-SMC). Thereby the CPS model described by SSTL can be verified in UPPAAL-SMC for spatial safety constraints. Finally, we illustrate the effectiveness of the approach in this article with a traffic alert and collision avoidance system.

Developers’ API needs should be more pragmatic, such as seeking suggestive, explainable, and extensible APIs rather than the so-called best result. Existing API search research cannot meet these pragmatic needs because they are solely concerned with query-API relevance. This necessitates a focus on enhancing the entire query process, from query definition to query refinement through intent clarification to query results promoting divergent thinking about results. This paper designs a novel Knowledge-Aware Human-AI Dialog agent (KAHAID) which guides the developer to clarify the uncertain, under-specified query through multi-round question answering and recommends APIs for the clarified query with relevance explanation and extended suggestions (e.g., alternative, collaborating or opposite-function APIs). We systematically evaluate KAHAID. In terms of human-AI dialogue process, it achieves a high diversity of question options (the average diversity between any two options is 74.9%) and the ability to guide developers to find APIs using fewer dialogue rounds (no more than 3 rounds on average). For API recommendation, KAHAID achieves an MRR and MAP of 0.769 and 0.794, outperforming state-of-the-art API search approaches BIKER and CLEAR by at least 47% in MRR and 226.7% in MAP. For knowledge extension, KAHAID obtains an MRR and MAP of 0.815 and 0.864, surpassing state-of-the-art query clarification approaches by at least 42% in MRR and 45.2% in MAP. As the first of its kind, KAHAID opens the door to integrating the immediate response capability of API research and the interaction, clarification, explanation, and extensibility capability of social-technical information seeking.

Programmers who work with smart contract development often encounter challenges in reusing code from repositories. This is due to the presence of two unknowns that can lead to non-functional and functional failures. These unknowns are implicit collaborations between functions and subtle differences among similar functions. Current code mining methods can extract syntax and semantic knowledge (known knowledge), but they cannot uncover these unknowns due to a significant gap between the known and the unknown. To address this issue, we formulate knowledge acquisition as a knowledge deduction task and propose an analytic flow that uses the function clone as a bridge to gradually deduce the known knowledge into the problem-solving knowledge that can reveal the unknowns. This flow comprises five methods: clone detection, co-occurrence probability calculation, function usage frequency accumulation, description propagation, and control flow graph annotation. This provides a systematic and coherent approach to knowledge deduction. We then structure all of the knowledge into a semantic-enriched code Knowledge Graph (KG) and integrate this KG into two software engineering tasks: code recommendation and crowd-scaled coding practice checking. As a proof of concept, we apply our approach to 5,140 smart contract files available on Etherscan.io and confirm high accuracy of our KG construction steps. In our experiments, our code KG effectively improved code recommendation accuracy by 6% to 45%, increased diversity by 61% to 102%, and enhanced NDCG by 1% to 21%. Furthermore, compared to traditional analysis tools and the debugging-with-the-crowd method, our KG improved time efficiency by 30 to 380 seconds, vulnerability determination accuracy by 20% to 33%, and vulnerability fixing accuracy by 24% to 40% for novice developers who identified and fixed vulnerable smart contract functions.

Software programming requires both API reference (know-what) knowledge and programming task (know-how) knowledge. Lots of programming know-what and know-how knowledge is documented in text, for example, API reference documentation and programming tutorials. To improve knowledge accessibility and usage, several recent studies use Natural Language Processing (NLP) methods to construct API know-what knowledge graph (API-KG) and programming task know-how knowledge graph (Task-KG) from software documentation. Although being promising, current API-KG and Task-KG are independent of each other, and thus are void of inherent connections between the two types of knowledge. Our empirical study on Stack Overflow questions confirms that only 36% of the API usage problems can be answered by the know-how or the know-what knowledge alone, while the rest questions requires a fusion of both. Inspired by this observation, we make the first attempt to fuse API-KG and Task-KG by API entity linking. This fusion creates nine categories of API semantic relations and two types of task semantic relations which are not present in the stand-alone API-KG or Task-KG. According to the definitions of these new API and task semantic relations, our approach dives deeper than surface-level API linking of API-KG and Task-KG, and infer nine categories of API semantic relations from task descriptions and two types of task semantic relations with the assistance of API-KG, which enrich the declaration or syntactic relations in the current API-KG and Task-KG. Our fused and semantically-enriched API-Task KG supports coherent API/Task-centric knowledge search by text or code queries. We have implemented our approach on Java programming documentation and built a web tool to search and explore API and programming task knowledge. Our evaluation confirms the high-accuracy of our knowledge extraction, fusion and enrichment methods, and the effectiveness and usefulness of our API-Task KG for answering Stack Overflow questions.

In this research, a new downscaling technique is developed for annual precipitation using the Global Precipitation Mission (GPM) based multitemporal weighted precipitation in Efficiency Distribution-based Framework (EDBF) algorithm. Two stepped methodology is adopted: Firstly, the assignment of weight to each temporal component based on the regression output in comparison with latitude; Secondly, to simulate the multitemporal weighted precipitiaon (e.g., the low-resolution at 0.75° resolution and the high-resolution at 0.05° resolution) in EDBF. Onward, predicted weighted precipitation is downscaled for annual precipitation, i.e., the year 2001, 2004 and the average annual precipitation (2001-2015) at 0.05° resolution, respectively. The downscaling approach resulting through proposed methodology captured the spatial patterns with greater accuracy at higher spatial resolution. This work showed that it is feasible to increase the spatial resolution of a precipitation variable(s) with greater accuracy on an annual basis or as an average from the multitemporal precipitation dataset through the weighted precipitation in EDBF algorithm.

Third-party libraries always evolve and produce multiple versions. Lucene, for example, released ten new versions (from version 7.7.0 to 8.4.0) in 2019. These versions confuse the existing code search methods to retrieve the source code that is not compatible with local programming language. To solve this issue, we propose DCSE, a deep code search model based on evolving information (i.e. evolved code tokens and evolution description). DCSE first deeply excavates evolved code tokens and evolution description in the code evolution process; then it takes evolved code tokens and evolution description as one feature of source code and code description, respectively. With such fuller representation, DCSE embeds source code and its code description into a high-dimensional shared vector space, and makes the cosine distance of their vectors closer. For the ever-evolving third-party libraries like Lucene, the experimental results show that DCSE could retrieve the source code that is compatible with local programming language, it outperforms the state-of-the-art methods (e.g. CODEnn) by 56.9–60.9[Formula: see text] in RFVersion. For the rarely-evolving third-party libraries, DCSE outperforms the state-of-the-art methods (e.g. CODEnn) by 4–11[Formula: see text] in Precision.

In this work, a Constraint Law method (CLM) based Genetic Algorithm (CLM-GA) is proposed for Nonlinear Least Square (LS) Regression and Normal Optimization Problems (NOP). Numerical experimental results show that CLM-GA is more robust than traditional methods (Gauss Newton, Levernberg Marquardt, EM-GA, EDBF-GA) for both LS and NOP problems in three aspects: 1) efficiency; 2) accuracy; 3) astringency. There are many LS and NOP applications in the physical world, such as military, economics, industry, photogrammetry and so on. Research of this paper can be easily implemented and applied for those applications.

The tree structure algorithms have been widely used in many computer fields. Developing efficient and reliable tree structure algorithms is a challenging problem in the field of software formalization and trusted software. In this paper, initially, the binary tree algorithms are divided into three kinds through induction of the loop invariant structures and output features. Then, PAR method can conveniently develop loop invariants and corresponding non-recursive algorithm programs. Finally, Isabelle is used to formally verify these developed algorithms. This development method not only overcomes the tediousness and error-proneness of traditional manual verification, but also greatly improves the efficiency and reliability of the developed algorithm program. To the best of our knowledge, this is the maiden attempt in the literature to verify a series of non-recursive and efficient binary tree algorithms. The above process forms a theorem proving library that include data types, data structures and lemma related binary tree algorithms, which can significantly reduce the cost of future verification.

The core of object-oriented programming (OOP) is the object, while the core of generic programming (GP) is the type requirement. Generic programming can improve the reusability, security and development efficiency of programs. Generic constraints can prevent run-time crashes of generic programs. Generics constraints and their matching mechanism in the mainstream programming languages are studied. The abstract degree of the current mainstream languages is not high enough to describe the complex dynamic semantic requirements. Abstract generic programming language Apla is used as the host language to propose a generic constraint method based on the type requirements of complete GP, including static syntax generic constraint and dynamic semantic generic constraint. A general generic constraint description language is given, a matching detection algorithm is designed to determine whether the static syntax generic constraints meet the requirements, and a matching verification mechanism is designed for dynamic semantic generic constraint verification. Finally, the whole process of matching detection and verification is demonstrated by taking Kleene algorithm as an example. The generic constraint mechanism can improve the security of the program. It further implements the GP concept with the type requirement as the core in the full sense.