Verification of Programs with Mutual Recursion in Pifagor Language View Full Text


Ontology type: schema:ScholarlyArticle     


Article Info

DATE

2018-12

AUTHORS

M. S. Ushakova, A. I. Legalov

ABSTRACT

In the article, we consider verification of programs with mutual recursion in the data driven functional parallel language Pifagor. In this language the program could be represented as a data flow graph, that has no control connections, and only has data relations. Under these conditions it is possible to simplify the process of formal verification, since there is no need to analyse resource conflicts, which are present in the systems with ordinary architectures. The proof of programs correctness is based on the elimination of mutual recursions by program transformation. The universal method of mutual recursion of an arbitrary number of functions elimination consists in constructing the universal recursive function that simulates all the functions in mutual recursion. A natural number is assigned to each function in mutual recursion. The universal recursive function takes as its argument the number of a function to be simulated and the arguments of this function. In some cases of the indirect recursion it is possible to use a simpler method of program transformation, namely, the merging of the functions code into a single function. To remove mutual recursion of an arbitrary number of functions, it is suggested to construct a graph of all connected functions and transform this graph by removing functions that are not connected with the target function, then by merging functions with indirect recursion and finally by constructing the universal recursive function. It is proved that in the Pifagor language such transformations of functions as code merging and universal recursive function construction do not change the correctness of the initial program. The example of partial correctness proof is given for the program that parses a simple arithmetic expression. We construct the graph of all connected functions and demonstrate two methods of proofs: by means of code merging and by means of the universal recursive function. More... »

PAGES

850-866

References to SciGraph publications

Identifiers

URI

http://scigraph.springernature.com/pub.10.3103/s0146411618070301

DOI

http://dx.doi.org/10.3103/s0146411618070301

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1112534970


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Siberian Federal University", 
          "id": "https://www.grid.ac/institutes/grid.412592.9", 
          "name": [
            "Siberian Federal University, Institute of Space and Information Technology, 660074, Krasnoyarsk, Russia"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Ushakova", 
        "givenName": "M. S.", 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Siberian Federal University", 
          "id": "https://www.grid.ac/institutes/grid.412592.9", 
          "name": [
            "Siberian Federal University, Institute of Space and Information Technology, 660074, Krasnoyarsk, Russia"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Legalov", 
        "givenName": "A. I.", 
        "type": "Person"
      }
    ], 
    "citation": [
      {
        "id": "sg:pub.10.3103/s0146411613070225", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1016018520", 
          "https://doi.org/10.3103/s0146411613070225"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf01209624", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1020487572", 
          "https://doi.org/10.1007/bf01209624"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/bf01209624", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1020487572", 
          "https://doi.org/10.1007/bf01209624"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-60360-3_38", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1021029713", 
          "https://doi.org/10.1007/3-540-60360-3_38"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0004-3702(94)90063-9", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1029915760"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1016/0004-3702(94)90063-9", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1029915760"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1023/a:1005797629953", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1035908543", 
          "https://doi.org/10.1023/a:1005797629953"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/363235.363259", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1043197262"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.1145/2692915.2628161", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1063164476"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "https://doi.org/10.18255/1818-1015-2015-4-578-589", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1068592122"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-52837-7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1109702472", 
          "https://doi.org/10.1007/3-540-52837-7"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-52837-7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1109702472", 
          "https://doi.org/10.1007/3-540-52837-7"
        ], 
        "type": "CreativeWork"
      }, 
      {
        "id": "sg:pub.10.1007/3-540-52837-7", 
        "sameAs": [
          "https://app.dimensions.ai/details/publication/pub.1109702472", 
          "https://doi.org/10.1007/3-540-52837-7"
        ], 
        "type": "CreativeWork"
      }
    ], 
    "datePublished": "2018-12", 
    "datePublishedReg": "2018-12-01", 
    "description": "In the article, we consider verification of programs with mutual recursion in the data driven functional parallel language Pifagor. In this language the program could be represented as a data flow graph, that has no control connections, and only has data relations. Under these conditions it is possible to simplify the process of formal verification, since there is no need to analyse resource conflicts, which are present in the systems with ordinary architectures. The proof of programs correctness is based on the elimination of mutual recursions by program transformation. The universal method of mutual recursion of an arbitrary number of functions elimination consists in constructing the universal recursive function that simulates all the functions in mutual recursion. A natural number is assigned to each function in mutual recursion. The universal recursive function takes as its argument the number of a function to be simulated and the arguments of this function. In some cases of the indirect recursion it is possible to use a simpler method of program transformation, namely, the merging of the functions code into a single function. To remove mutual recursion of an arbitrary number of functions, it is suggested to construct a graph of all connected functions and transform this graph by removing functions that are not connected with the target function, then by merging functions with indirect recursion and finally by constructing the universal recursive function. It is proved that in the Pifagor language such transformations of functions as code merging and universal recursive function construction do not change the correctness of the initial program. The example of partial correctness proof is given for the program that parses a simple arithmetic expression. We construct the graph of all connected functions and demonstrate two methods of proofs: by means of code merging and by means of the universal recursive function.", 
    "genre": "research_article", 
    "id": "sg:pub.10.3103/s0146411618070301", 
    "inLanguage": [
      "en"
    ], 
    "isAccessibleForFree": false, 
    "isFundedItemOf": [
      {
        "id": "sg:grant.5347590", 
        "type": "MonetaryGrant"
      }
    ], 
    "isPartOf": [
      {
        "id": "sg:journal.1136763", 
        "issn": [
          "0146-4116", 
          "1558-108X"
        ], 
        "name": "Automatic Control and Computer Sciences", 
        "type": "Periodical"
      }, 
      {
        "issueNumber": "7", 
        "type": "PublicationIssue"
      }, 
      {
        "type": "PublicationVolume", 
        "volumeNumber": "52"
      }
    ], 
    "name": "Verification of Programs with Mutual Recursion in Pifagor Language", 
    "pagination": "850-866", 
    "productId": [
      {
        "name": "readcube_id", 
        "type": "PropertyValue", 
        "value": [
          "5fc6aead79e89b9d2fc7e1919bd49658b204ba658fcf89e1dabed90865001cd2"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.3103/s0146411618070301"
        ]
      }, 
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1112534970"
        ]
      }
    ], 
    "sameAs": [
      "https://doi.org/10.3103/s0146411618070301", 
      "https://app.dimensions.ai/details/publication/pub.1112534970"
    ], 
    "sdDataset": "articles", 
    "sdDatePublished": "2019-04-11T11:00", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-uberresearch-data-dimensions-target-20181106-alternative/cleanup/v134/2549eaecd7973599484d7c17b260dba0a4ecb94b/merge/v9/a6c9fde33151104705d4d7ff012ea9563521a3ce/jats-lookup/v90/0000000352_0000000352/records_60338_00000004.jsonl", 
    "type": "ScholarlyArticle", 
    "url": "https://link.springer.com/10.3103%2FS0146411618070301"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.3103/s0146411618070301'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.3103/s0146411618070301'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.3103/s0146411618070301'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.3103/s0146411618070301'


 

This table displays all metadata directly associated to this object as RDF triples.

100 TRIPLES      21 PREDICATES      36 URIs      19 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.3103/s0146411618070301 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N6a5e9f72559a40baa52610ea4d377d73
4 schema:citation sg:pub.10.1007/3-540-52837-7
5 sg:pub.10.1007/3-540-60360-3_38
6 sg:pub.10.1007/bf01209624
7 sg:pub.10.1023/a:1005797629953
8 sg:pub.10.3103/s0146411613070225
9 https://doi.org/10.1016/0004-3702(94)90063-9
10 https://doi.org/10.1145/2692915.2628161
11 https://doi.org/10.1145/363235.363259
12 https://doi.org/10.18255/1818-1015-2015-4-578-589
13 schema:datePublished 2018-12
14 schema:datePublishedReg 2018-12-01
15 schema:description In the article, we consider verification of programs with mutual recursion in the data driven functional parallel language Pifagor. In this language the program could be represented as a data flow graph, that has no control connections, and only has data relations. Under these conditions it is possible to simplify the process of formal verification, since there is no need to analyse resource conflicts, which are present in the systems with ordinary architectures. The proof of programs correctness is based on the elimination of mutual recursions by program transformation. The universal method of mutual recursion of an arbitrary number of functions elimination consists in constructing the universal recursive function that simulates all the functions in mutual recursion. A natural number is assigned to each function in mutual recursion. The universal recursive function takes as its argument the number of a function to be simulated and the arguments of this function. In some cases of the indirect recursion it is possible to use a simpler method of program transformation, namely, the merging of the functions code into a single function. To remove mutual recursion of an arbitrary number of functions, it is suggested to construct a graph of all connected functions and transform this graph by removing functions that are not connected with the target function, then by merging functions with indirect recursion and finally by constructing the universal recursive function. It is proved that in the Pifagor language such transformations of functions as code merging and universal recursive function construction do not change the correctness of the initial program. The example of partial correctness proof is given for the program that parses a simple arithmetic expression. We construct the graph of all connected functions and demonstrate two methods of proofs: by means of code merging and by means of the universal recursive function.
16 schema:genre research_article
17 schema:inLanguage en
18 schema:isAccessibleForFree false
19 schema:isPartOf N30d18d8c595f4b1eaafa67b4f86dea0d
20 N3d014a450e2b40cb9858fad0c826da0e
21 sg:journal.1136763
22 schema:name Verification of Programs with Mutual Recursion in Pifagor Language
23 schema:pagination 850-866
24 schema:productId Nc24e2328485c4fc5bd5bcb102e877554
25 Ncc30c1c3d75542208303fb37bf734a6a
26 Ndf765187500f459eb3d342b5cbcbe757
27 schema:sameAs https://app.dimensions.ai/details/publication/pub.1112534970
28 https://doi.org/10.3103/s0146411618070301
29 schema:sdDatePublished 2019-04-11T11:00
30 schema:sdLicense https://scigraph.springernature.com/explorer/license/
31 schema:sdPublisher N3944058584be43c4b8e6ae2d1ef1118d
32 schema:url https://link.springer.com/10.3103%2FS0146411618070301
33 sgo:license sg:explorer/license/
34 sgo:sdDataset articles
35 rdf:type schema:ScholarlyArticle
36 N30d18d8c595f4b1eaafa67b4f86dea0d schema:volumeNumber 52
37 rdf:type schema:PublicationVolume
38 N3944058584be43c4b8e6ae2d1ef1118d schema:name Springer Nature - SN SciGraph project
39 rdf:type schema:Organization
40 N3d014a450e2b40cb9858fad0c826da0e schema:issueNumber 7
41 rdf:type schema:PublicationIssue
42 N6a5e9f72559a40baa52610ea4d377d73 rdf:first Nc7a84bc1bb484083a0e189a9ce18e1b5
43 rdf:rest Nfc331c76a555442aaf348cefdf6d0e36
44 Nc24e2328485c4fc5bd5bcb102e877554 schema:name dimensions_id
45 schema:value pub.1112534970
46 rdf:type schema:PropertyValue
47 Nc7a84bc1bb484083a0e189a9ce18e1b5 schema:affiliation https://www.grid.ac/institutes/grid.412592.9
48 schema:familyName Ushakova
49 schema:givenName M. S.
50 rdf:type schema:Person
51 Ncc30c1c3d75542208303fb37bf734a6a schema:name doi
52 schema:value 10.3103/s0146411618070301
53 rdf:type schema:PropertyValue
54 Ndf765187500f459eb3d342b5cbcbe757 schema:name readcube_id
55 schema:value 5fc6aead79e89b9d2fc7e1919bd49658b204ba658fcf89e1dabed90865001cd2
56 rdf:type schema:PropertyValue
57 Ne54b8e7612134102a153a6a2047b75c5 schema:affiliation https://www.grid.ac/institutes/grid.412592.9
58 schema:familyName Legalov
59 schema:givenName A. I.
60 rdf:type schema:Person
61 Nfc331c76a555442aaf348cefdf6d0e36 rdf:first Ne54b8e7612134102a153a6a2047b75c5
62 rdf:rest rdf:nil
63 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
64 schema:name Information and Computing Sciences
65 rdf:type schema:DefinedTerm
66 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
67 schema:name Computation Theory and Mathematics
68 rdf:type schema:DefinedTerm
69 sg:grant.5347590 http://pending.schema.org/fundedItem sg:pub.10.3103/s0146411618070301
70 rdf:type schema:MonetaryGrant
71 sg:journal.1136763 schema:issn 0146-4116
72 1558-108X
73 schema:name Automatic Control and Computer Sciences
74 rdf:type schema:Periodical
75 sg:pub.10.1007/3-540-52837-7 schema:sameAs https://app.dimensions.ai/details/publication/pub.1109702472
76 https://doi.org/10.1007/3-540-52837-7
77 rdf:type schema:CreativeWork
78 sg:pub.10.1007/3-540-60360-3_38 schema:sameAs https://app.dimensions.ai/details/publication/pub.1021029713
79 https://doi.org/10.1007/3-540-60360-3_38
80 rdf:type schema:CreativeWork
81 sg:pub.10.1007/bf01209624 schema:sameAs https://app.dimensions.ai/details/publication/pub.1020487572
82 https://doi.org/10.1007/bf01209624
83 rdf:type schema:CreativeWork
84 sg:pub.10.1023/a:1005797629953 schema:sameAs https://app.dimensions.ai/details/publication/pub.1035908543
85 https://doi.org/10.1023/a:1005797629953
86 rdf:type schema:CreativeWork
87 sg:pub.10.3103/s0146411613070225 schema:sameAs https://app.dimensions.ai/details/publication/pub.1016018520
88 https://doi.org/10.3103/s0146411613070225
89 rdf:type schema:CreativeWork
90 https://doi.org/10.1016/0004-3702(94)90063-9 schema:sameAs https://app.dimensions.ai/details/publication/pub.1029915760
91 rdf:type schema:CreativeWork
92 https://doi.org/10.1145/2692915.2628161 schema:sameAs https://app.dimensions.ai/details/publication/pub.1063164476
93 rdf:type schema:CreativeWork
94 https://doi.org/10.1145/363235.363259 schema:sameAs https://app.dimensions.ai/details/publication/pub.1043197262
95 rdf:type schema:CreativeWork
96 https://doi.org/10.18255/1818-1015-2015-4-578-589 schema:sameAs https://app.dimensions.ai/details/publication/pub.1068592122
97 rdf:type schema:CreativeWork
98 https://www.grid.ac/institutes/grid.412592.9 schema:alternateName Siberian Federal University
99 schema:name Siberian Federal University, Institute of Space and Information Technology, 660074, Krasnoyarsk, Russia
100 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...