GLORIA

GEOMAR Library Ocean Research Information Access

X

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
  • EDP Sciences  (5)
  • 1
    Online Resource
    Online Resource
    Course Intelligent Brain Model Based on Crowd Intelligence
    EDP Sciences ; 2022
    In:  Wuhan University Journal of Natural Sciences Vol. 27, No. 4 ( 2022-08), p. 331-340
    Details
    In: Wuhan University Journal of Natural Sciences, EDP Sciences, Vol. 27, No. 4 ( 2022-08), p. 331-340
    Abstract: The development of artificial intelligence in education promotes the reform of teaching methods in the direction of intelligence and individuation. In this paper, the programming course is taken as an example to propose a curriculum intelligent brain model for open source swarm intelligence based on knowledge graph, and the bootstrapping framework is introduced to try to make the intelligent brain track the frontier like human beings and study several courses vertically. It studies the knowledge of subgraphs fusion of open-source software resources and domain semantics as well as the mining method of potential relationship, so that the intelligent brain can digest knowledge like human, and get through the course horizontally. Finally, knowledge discovery and natural representation based on knowledge graph enable intelligent brain to discover knowledge and solve problems just like human. This study provides new ideas, strategies, and application paths for the construction of knowledge graph based on big data and the integration of heterogeneous knowledge graph.
    Type of Medium: Online Resource
    ISSN: 1007-1202 , 1993-4998
    URL: Article
    DOI: 10.1051/wujns/2022274331
    Language: English
    Publisher: EDP Sciences
    Publication Date: 2022
    detail.hit.zdb_id: 2365459-4
    SSG: 11
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 2
    Online Resource
    Online Resource
    A Unified Strategy for Formal Derivation and Proof of Binary Tree Nonrecursive Algorithms
    EDP Sciences ; 2022
    In:  Wuhan University Journal of Natural Sciences Vol. 27, No. 5 ( 2022-10), p. 415-423
    Details
    In: Wuhan University Journal of Natural Sciences, EDP Sciences, Vol. 27, No. 5 ( 2022-10), p. 415-423
    Abstract: In the formal derivation and proof of binary tree algorithms, Dijkstra's weakest predicate method is commonly used. However, the method has some drawbacks, including a time-consuming derivation process, complicated loop invariants, and the inability to generate executable programs from the specification. This paper proposes a unified strategy for the formal derivation and proof of binary tree non-recursive algorithms to address these issues. First, binary tree problem solving sequences are decomposed into two types of recursive relations based on queue and stack, and two corresponding loop invariant templates are constructed. Second, high-reliability Apla (abstract programming language) programs are derived using recursive relations and loop invariants. Finally, Apla programs are converted automatically into C++ executable programs. Two types of problems with binary tree queue and stack recursive relations are used as examples, and their formal derivation and proof are performed to validate the proposed strategy's effectiveness. This strategy improves the efficiency and correctness of binary tree algorithm derivation.
    Type of Medium: Online Resource
    ISSN: 1007-1202 , 1993-4998
    URL: Article
    DOI: 10.1051/wujns/2022275415
    Language: English
    Publisher: EDP Sciences
    Publication Date: 2022
    detail.hit.zdb_id: 2365459-4
    SSG: 11
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 3
    Online Resource
    Online Resource
    A Method to Deduce and Synthesize the Dafny Programs
    EDP Sciences ; 2021
    In:  Wuhan University Journal of Natural Sciences Vol. 26, No. 6 ( 2021-12), p. 481-488
    Details
    In: Wuhan University Journal of Natural Sciences, EDP Sciences, Vol. 26, No. 6 ( 2021-12), p. 481-488
    Abstract: 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.
    Type of Medium: Online Resource
    ISSN: 1007-1202 , 1993-4998
    URL: Article
    DOI: 10.1051/wujns/2021266481
    Language: English
    Publisher: EDP Sciences
    Publication Date: 2021
    detail.hit.zdb_id: 2365459-4
    SSG: 11
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 4
    Online Resource
    Online Resource
    Automatic Algorithm Programming Model Based on the Improved Morgan's Refinement Calculus
    EDP Sciences ; 2022
    In:  Wuhan University Journal of Natural Sciences Vol. 27, No. 5 ( 2022-10), p. 405-414
    Details
    In: Wuhan University Journal of Natural Sciences, EDP Sciences, Vol. 27, No. 5 ( 2022-10), p. 405-414
    Abstract: The automatic algorithm programming model can increase the dependability and efficiency of algorithm program development, including specification generation, program refinement, and formal verification. However, the existing model has two flaws: incompleteness of program refinement and inadequate automation of formal verification. This paper proposes an automatic algorithm programming model based on the improved Morgan's refinement calculus. It extends the Morgan's refinement calculus rules and designs the C++ generation system for realizing the complete process of refinement. Meanwhile, the automation tools VCG (Verification Condition Generator) and Isabelle are used to improve the automation of formal verification. An example of a stock's maximum income demonstrates the effectiveness of the proposed model. Furthermore, the proposed model has some relevance for automatic software generation.
    Type of Medium: Online Resource
    ISSN: 1007-1202 , 1993-4998
    URL: Article
    DOI: 10.1051/wujns/2022275405
    Language: English
    Publisher: EDP Sciences
    Publication Date: 2022
    detail.hit.zdb_id: 2365459-4
    SSG: 11
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
  • 5
    Online Resource
    Online Resource
    Nonlinear Program Construction and Verification Method Based on Partition Recursion and Morgan's Refinement Rules
    EDP Sciences ; 2023
    In:  Wuhan University Journal of Natural Sciences Vol. 28, No. 3 ( 2023-06), p. 246-256
    Details
    In: Wuhan University Journal of Natural Sciences, EDP Sciences, Vol. 28, No. 3 ( 2023-06), p. 246-256
    Abstract: The traditional program refinement strategy cannot be refined to an executable program, and there are issues such as low verification reliability and automation. To solve the above problems, this paper proposes a nonlinear program construction and verification method based on partition recursion and Morgan's refinement rules. First, we use recursive definition technique to characterize the initial specification. The specification is then transformed into GCL(Guarded Command Language) programs using loop invariant derivation and Morgan's refinement rules. Furthermore, VCG (Verification Condition Generator) is used in the GCL program to generate the verification condition automatically. The Isabelle theorem prover then validates the GCL program's correctness. Finally, the GCL code generates a C++ executable program automatically via the conversion system. The effectiveness of this method is demonstrated using binary tree preorder traversal program construction and verification as an example. This method addresses the problem that the construction process's loop invariant is difficult to obtain and the refinement process is insufficiently detailed. At the same time, the method improves verification process automation and reduces the manual verification workload.
    Type of Medium: Online Resource
    ISSN: 1007-1202 , 1993-4998
    URL: Article
    DOI: 10.1051/wujns/2023283246
    Language: English
    Publisher: EDP Sciences
    Publication Date: 2023
    detail.hit.zdb_id: 2365459-4
    SSG: 11
    Location Call Number Limitation Availability
    BibTip Others were also interested in ...
    Online Resource
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...