IDEAS home Printed from https://ideas.repec.org/a/eee/matcom/v79y2009i8p2302-2309.html
   My bibliography  Save this article

Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs

Author

Listed:
  • Popov, Nikolaj
  • Jebelean, Tudor

Abstract

We describe an innovative method for proving total correctness of tail recursive programs having a specific structure, namely programs in which an auxiliary tail recursive function is driven by a main nonrecursive function, and only the specification of the main function is provided. The specification of the auxiliary function is obtained almost fully automatically by solving coupled linear recursive sequences with constant coefficients. The process is carried out by means of CA (Computer Algebra) and AC (Algorithmic Combinatorics) and is implemented in the Theorema system (using Mathematica). We demonstrate this method on an example involving polynomial expressions. Furthermore, we develop a method for synthesis of recursive programs for computing polynomial expressions of a fixed degree by means of “cheap” operations, e.g., additions, subtractions and multiplications. For a given polynomial expression, we define its recursive program in a schemewise manner. The correctness of the synthesized programs follows from the general correctness of the synthesis method, which is proven once for all, using the verification method presented in the first part of this paper.

Suggested Citation

  • Popov, Nikolaj & Jebelean, Tudor, 2009. "Using Computer Algebra techniques for the specification, verification and synthesis of recursive programs," Mathematics and Computers in Simulation (MATCOM), Elsevier, vol. 79(8), pages 2302-2309.
    • Handle: RePEc:eee:matcom:v:79:y:2009:i:8:p:2302-2309
    DOI: 10.1016/j.matcom.2008.11.017
    as

    Download full text from publisher

    File URL: http://www.sciencedirect.com/science/article/pii/S037847540800373X
    Download Restriction: Full text for ScienceDirect subscribers only
    File URL: https://libkey.io/10.1016/j.matcom.2008.11.017?utm_source=ideas
    LibKey link: if access is restricted and if your library uses this service, LibKey will redirect you to where you can use your library subscription to access this item
    ---><---

    As the access to this document is restricted, you may want to search for a different version of it.

    References listed on IDEAS

    as
    1. Polterovich, Victor & Popov, Vladimir, 2006. "Эволюционная Теория Экономической Политики: Часть I: Опыт Быстрого Развития [An Evolutionary Theory of Economic Policy: Part I: The Experience of Fast Development]," MPRA Paper 22168, University Library of Munich, Germany.
    Full references (including those not matched with items on IDEAS)

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Kritana Prueksakorn & Cheng-Xu Piao & Hyunchul Ha & Taehyeung Kim, 2015. "Computational and Experimental Investigation for an Optimal Design of Industrial Windows to Allow Natural Ventilation during Wind-Driven Rain," Sustainability, MDPI, vol. 7(8), pages 1-22, August.
    2. Grzegorz W. Kolodko, 2009. "A Two-thirds Rate of Success: Polish Transformation and Economic Development, 1989-2008," WIDER Working Paper Series RP2009-14, World Institute for Development Economic Research (UNU-WIDER).
    3. Kudrin, A. & Gurvich, E., 2015. "Government Stimulus or Economic Incentives?," Journal of the New Economic Association, New Economic Association, vol. 26(2), pages 179-186.
    4. Larysa Tamilina & Natalya Tamilina, 2014. "Heterogeneity in Institutional Effects on Economic Growth: Theory and Empirical Evidence," European Journal of Comparative Economics, Cattaneo University (LIUC), vol. 11(2), pages 205-249, December.
    5. Sturm, J. & Ennifar, H. & Erhard, S.V. & Rheinfeld, A. & Kosch, S. & Jossen, A., 2018. "State estimation of lithium-ion cells using a physicochemical model based extended Kalman filter," Applied Energy, Elsevier, vol. 223(C), pages 103-123.
    6. repec:mje:mjejnl:v:12:y:2017:i:1:p:125-140 is not listed on IDEAS
    7. Okur, Osman & Alper, Erdogan & Almansoori, Ali, 2014. "Optimization of catalyst preparation conditions for direct sodium borohydride fuel cell using response surface methodology," Energy, Elsevier, vol. 67(C), pages 97-105.
    8. Adam S. Posen & Daniel Popov Gould, 2007. "Has EMU Had Any Impact on the Degree of Wage Restraint?," Palgrave Macmillan Books, in: David Cobham (ed.), The Travails of the Eurozone, chapter 7, pages 146-178, Palgrave Macmillan.
    9. Popov, V., 2011. "Do We Need to Protect Intellectual Property Rights?," Journal of the New Economic Association, New Economic Association, issue 11, pages 107-126.
    10. Mo, Jingke & Kang, Zhenye & Yang, Gaoqiang & Retterer, Scott T. & Cullen, David A. & Toops, Todd J. & Green, Johney B. & Zhang, Feng-Yuan, 2016. "Thin liquid/gas diffusion layers for high-efficiency hydrogen production from water splitting," Applied Energy, Elsevier, vol. 177(C), pages 817-822.
    11. Cang, Shuang & Yu, Hongnian, 2014. "A combination selection algorithm on forecasting," European Journal of Operational Research, Elsevier, vol. 234(1), pages 127-139.
    12. Challet, Damien & Solomon, Sorin & Yaari, Gur, 2009. "The universal shape of economic recession and recovery after a shock," Economics - The Open-Access, Open-Assessment E-Journal (2007-2020), Kiel Institute for the World Economy (IfW Kiel), vol. 3, pages 1-24.
    13. Ermete Antolini, 2017. "Pt-Ni and Pt-M-Ni (M = Ru, Sn) Anode Catalysts for Low-Temperature Acidic Direct Alcohol Fuel Cells: A Review," Energies, MDPI, vol. 10(1), pages 1-20, January.
    14. Holvoet, Katrijn M.A. & Seuntjens, Piet & Vanrolleghem, Peter A., 2007. "Monitoring and modeling pesticide fate in surface waters at the catchment scale," Ecological Modelling, Elsevier, vol. 209(1), pages 53-64.
    15. Jinsoo Park & Jung-Il Choi & Gwang Hoon Rhee, 2016. "Enhanced Single-Sided Ventilation with Overhang in Buildings," Energies, MDPI, vol. 9(3), pages 1-14, February.
    16. Jung, Guo-Bin & Tzeng, Wei-Jen & Jao, Ting-Chu & Liu, Yu-Hsu & Yeh, Chia-Chen, 2013. "Investigation of porous carbon and carbon nanotube layer for proton exchange membrane fuel cells," Applied Energy, Elsevier, vol. 101(C), pages 457-464.
    17. Estache, Antonio & Rossi, Martin A., 2008. "Regulatory agencies : impact on firm performance and social welfare," Policy Research Working Paper Series 4509, The World Bank.
    18. Roudbari, Mohsen Najafi & Ojani, Reza & Raoof, Jahan Bakhsh, 2019. "Performance improvement of polymer fuel cell by simultaneously inspection of catalyst loading, catalyst content and ionomer using home-made cathodic half-cell and response surface method," Energy, Elsevier, vol. 173(C), pages 151-161.
    19. Popov, Vladimir & Chowdhury, Anis, 2015. "What Uzbekistan tells us about industrial policy that we did not know?," MPRA Paper 67013, University Library of Munich, Germany.
    20. Mojović, Ljiljana & Pejin, Dušanka & Rakin, Marica & Pejin, Jelena & Nikolić, Svetlana & Djukić-Vuković, Aleksandra, 2012. "How to improve the economy of bioethanol production in Serbia," Renewable and Sustainable Energy Reviews, Elsevier, vol. 16(8), pages 6040-6047.
    21. A. Vissarionov B. & R. Gumerov R. & АЛЕКСАНДР Виссарионов БОРИСОВИЧ & РУСТАМ Гумеров РАУЛЕВИЧ, 2017. "Об использовании предельных (пороговых) значений индикаторов экономической безопасности Российской Федерации // Concerning the Use of Indicators’ Marginal (Threshold) Values of the Russian Federation ," Управленческие науки // Management Science, ФГОБУВО Финансовый университет при Правительстве Российской Федерации // Financial University under The Government of Russian Federation, vol. 7(3), pages 12-20.

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:eee:matcom:v:79:y:2009:i:8:p:2302-2309. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Catherine Liu (email available below). General contact details of provider: http://www.journals.elsevier.com/mathematics-and-computers-in-simulation/ .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.