Piton pp 43-70 | Cite as

Big Number Addition

Part of the Automated Reasoning Series book series (ARSE, volume 3)


In this chapter we consider an example programming problem and its solution in Piton. The problem is to specify, implement, and verify a program for doing “big number addition.” This chapter is a rather long but instructive detour from our main goal of implementing Piton on FM9001 and proving the implementation correct.


Data Segment Data Area Main Program Symbolic Execution Program Counter 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Kluwer Academic Publishers 1996

Personalised recommendations