The paper presents a formal and practical approach to dependable algorithm development.First,starting from a formal specification based on the Eindhoven quantifier notation,a problem is regularly reduced to subproblem...The paper presents a formal and practical approach to dependable algorithm development.First,starting from a formal specification based on the Eindhoven quantifier notation,a problem is regularly reduced to subproblems with less complexity by using a concise set of calculation rules,the result of which establishes a recurrence-based algorithm.Second,a loop invariant is derived from the problem specification and recurrence,which certifies the transformation from the recurrence-based algorithm to one or more iterative programs.We demonstrate that our approach covers a number of classical algorithm design tactics,develops algorithmic programs together with their proof of correctness,and thus contributes fundamentally to the dependability of computer software.展开更多
Sparse signal recovery is a topic of considerable interest,and the literature in this field is already quite immense.Many problems that arise in sparse signal recovery can be generalized as a convex programming with l...Sparse signal recovery is a topic of considerable interest,and the literature in this field is already quite immense.Many problems that arise in sparse signal recovery can be generalized as a convex programming with linear conic constraints.In this paper,we present a new proximal point algorithm(PPA) termed as relaxed-PPA(RPPA) contraction method,for solving this common convex programming.More precisely,we first reformulate the convex programming into an equivalent variational inequality(VI),and then efficiently explore its inner structure.In each step,our method relaxes the VI-subproblem to a tractable one,which can be solved much more efficiently than the original VI.Under mild conditions,the convergence of the proposed method is proved.Experiments with l1 analysis show that RPPA is a computationally efficient algorithm and compares favorably with the recently proposed state-of-the-art algorithms.展开更多
Partition-and-Recur (PAR) method is a simple and useful formal method. It can be used to design and testify algo-rithmic programs. In this paper, we propose that PAR method is an effective formal method on solving com...Partition-and-Recur (PAR) method is a simple and useful formal method. It can be used to design and testify algo-rithmic programs. In this paper, we propose that PAR method is an effective formal method on solving combinatorics problems. Furthermore, we formally derive combinatorics problems by PAR method, which cannot only simplify the process of algorithmic program's designing, but also improve its automatization, standardization and correctness. We develop algorithms for two typical combinatorics problems, the number of string scheme and the number of error per-mutation scheme. Lastly, we obtain accurate C++ programs which are transformed by automatic transforming system of PAR platform.展开更多
基金National Natural Science Foundation of China under Grant No. 60773054,60870002 and 61020106009Zhejiang Provincial Natural Science Foundation of China under Grant No. R1110679
文摘The paper presents a formal and practical approach to dependable algorithm development.First,starting from a formal specification based on the Eindhoven quantifier notation,a problem is regularly reduced to subproblems with less complexity by using a concise set of calculation rules,the result of which establishes a recurrence-based algorithm.Second,a loop invariant is derived from the problem specification and recurrence,which certifies the transformation from the recurrence-based algorithm to one or more iterative programs.We demonstrate that our approach covers a number of classical algorithm design tactics,develops algorithmic programs together with their proof of correctness,and thus contributes fundamentally to the dependability of computer software.
基金the National Natural Science Foundation of China(No.70901018)
文摘Sparse signal recovery is a topic of considerable interest,and the literature in this field is already quite immense.Many problems that arise in sparse signal recovery can be generalized as a convex programming with linear conic constraints.In this paper,we present a new proximal point algorithm(PPA) termed as relaxed-PPA(RPPA) contraction method,for solving this common convex programming.More precisely,we first reformulate the convex programming into an equivalent variational inequality(VI),and then efficiently explore its inner structure.In each step,our method relaxes the VI-subproblem to a tractable one,which can be solved much more efficiently than the original VI.Under mild conditions,the convergence of the proposed method is proved.Experiments with l1 analysis show that RPPA is a computationally efficient algorithm and compares favorably with the recently proposed state-of-the-art algorithms.
文摘Partition-and-Recur (PAR) method is a simple and useful formal method. It can be used to design and testify algo-rithmic programs. In this paper, we propose that PAR method is an effective formal method on solving combinatorics problems. Furthermore, we formally derive combinatorics problems by PAR method, which cannot only simplify the process of algorithmic program's designing, but also improve its automatization, standardization and correctness. We develop algorithms for two typical combinatorics problems, the number of string scheme and the number of error per-mutation scheme. Lastly, we obtain accurate C++ programs which are transformed by automatic transforming system of PAR platform.
