Changeset 1576 for trunk


Ignore:
Timestamp:
Aug 21, 2019 2:28:12 PM (5 years ago)
Author:
magne
Message:

Makefile

  • Changed axiom names according to Mathematics.Numbers.

BasicCxx.DynamicArrayCxx

  • Replaced problematic cases of accessing struct components with more elaborate code.
  • Removed some obsolete operations.
  • Improved documentation.

BasicCxxExamples.LoopsCxxDemo

  • Added Cxx suffixes to runnable code.
  • Fixed some renaming problems.
  • Improved documentation.

BasicCxxRaw.RepetitionCountCxxRawTest

  • Added Cxx suffixes to runnable code.
  • Fixed some renaming problems.

BasicGeneral.ArrayFilterCxxDemo

  • Improved naming scheme of runnable code.

BasicGeneral.IntegerOperations

  • Replaced problematic cases of accessing struct components with more elaborate code.

Mathematics.Numbers

  • Changed axiom name to naturalLogarithmPowAxiom.

TutorialExamples.Tutorial0Cxx

  • Improved documentation.

TutorialExamples.Tutorial3Cxx

  • Added more example code.

TutorialExamples.Tutorial4Cxx

  • Improved documentation.
  • Replaced problematic cases of accessing struct components with more elaborate code.

TutorialExamples.Tutorial9Cxx

  • Improved documentation.
  • Replaced problematic cases of accessing struct components with more elaborate code.
Location:
trunk/magnolia-basic-library/src
Files:
11 edited

Legend:

Unmodified
Added
Removed

  • trunk/magnolia-basic-library/src/BasicCxx/DynamicArrayCxx.mg

    r1454 r1576  
    4545  predicate accessible ( a:A, i:Intex ) = zerointex() <= i && i < a.size;
    4646
    47   /** replace current value of the element at the given index of the array. */
     47  /** Replace current value of the element at the given index of the array.
     48   * Enlarge {@code a} if the new element is exactly at its end.
     49   */
    4850  procedure change ( upd a:A, obs i:Intex, obs e:E )
    49     guard (accessible(a,i) || i == getSize(a)) && getSize(a) != maximumintex() {
     51    guard (accessible(a,i) || i == getSize(a)) && getSize(a) != maximumintex()
     52  { var a_size = a.size;
    5053    if i == bar_getSize(a.data)
    51     then call enlarge_array(a,i+oneintex());
    52     end;
    53     call bar_replaceSegment(a.data,i,i+oneintex(),e);
    54     if i == a.size then a.size = a.size + oneintex(); end;
     54    then
     55      assert i == a_size;
     56      var new_s = i + i + oneintex();
     57      var new_d = bar_createArray_element(new_s,e);
     58      call bar_replaceSegmentFromArray(new_d,zerointex(),a.size,a.data,zerointex());
     59      a.size = i + oneintex();
     60      a.data = new_d;
     61    else
     62      var new_d = a.data;
     63      call bar_replaceSegment(new_d,i,i+oneintex(),e);
     64      a.size = if i == a_size then a_size + oneintex() else a_size end;
     65      a.data = new_d;
     66    end;
    5567  };
    5668
    5769  /** Concatenate elements of second array to the first at position {@code k} onwards, as far as possible. */
    5870  procedure concatenate( upd a1:A, obs a2:A )
    59     guard getSize(a1) != maximumintex() && getSize(a2) != maximumintex() {
    60     var a = a1.size+a2.size;
    61     if( a > bar_getSize(a1.data) )
    62     then call enlarge_array (a1,a);
    63     end;
    64     call bar_concatenate(a1.data,a1.size,a2.data,a2.size);
    65     a1.size = a;
     71    guard getSize(a1) + getSize(a2) < maximumintex()
     72  { var a_sum = a1.size + a2.size;
     73    if a_sum <= bar_getSize(a1.data)
     74    then
     75      var new_d = a1.data;
     76      call bar_replaceSegmentFromArray( new_d, a1.size, a_sum, a2.data, zerointex() );
     77      a1.data = new_d;
     78    else
     79      if a1.size == zerointex()
     80      then
     81        a1.data = a2.data;
     82      else
     83        var new_s = bar_getSize(a1.data) + bar_getSize(a2.data) + oneintex();
     84        var new_d = bar_createArray_element(new_s,bar_getElement(a1.data,zerointex()));
     85        call bar_replaceSegmentFromArray(new_d,oneintex(),a1.size,a1.data,oneintex());
     86        call bar_replaceSegmentFromArray(new_d,a1.size,a_sum,a2.data,zerointex());
     87        a1.data = new_d;
     88      end;
     89    end;
     90    a1.size = a_sum;
    6691  };
    6792 
    … …  
    86111  /** Deletes an element of the array. */
    87112  procedure delete( upd a:A, obs i:Intex )
    88     guard zerointex() <= i && i < getSize(a) && getSize(a) != maximumintex() {
     113    guard zerointex() <= i && i < getSize(a) && getSize(a) != maximumintex()
     114  { var a_size = a.size;
     115    var new_d = a.data;
    89116    // Moves element to be deleted to last position.
    90     call bar_shiftSegmentGroups(a.data,a.size-i,oneintex(),oneintex(),i,a.size);
     117    call bar_shiftSegmentGroups(new_d,a_size-i,oneintex(),oneintex(),i,a_size);
    91118    // Effectively deletes last element.
    92     a.size = a.size - oneintex();
     119    a.size = a_size - oneintex();
     120    a.data = new_d;
    93121  };
    94122 
    … …  
    120148    zerointex() < k && mod(a.size,k) == zerointex() && zerointex() <= i && k*i <= a.size && a.size != maximumintex();
    121149 
    122   /** replace current value of the element at the given index of the array. */
     150  /** Insert value of the element at the given index of the array, pushing the remaining elements one step down. */
    123151  procedure insert ( upd a:A, obs i:Intex, obs e:E )
    124     guard zerointex() <= i && i <= getSize(a) && getSize(a) != maximumintex() {
    125     // Insert new element at the back.
    126     call change(a,getSize(a),e);
    127     // Rotate latter part to move into right position
    128     call bar_shiftSegmentGroups(a.data,a.size-i,oneintex(),a.size-i-oneintex(),i,a.size);
    129   };
    130 
    131   /** Replace the elements within the given bounds to the argument value @code{e}. */
     152    guard zerointex() <= i && i <= getSize(a) && getSize(a) != maximumintex()
     153  {
     154    var a_size = a.size + oneintex();
     155    if  bar_getSize(a.data) < a_size
     156    then // Needs to extend the underlying array.
     157      var new_s = a_size + a_size + oneintex();
     158      var new_d = bar_createArray_element(new_s,e);
     159      call bar_replaceSegmentFromArray(new_d,zerointex(),i,a.data,zerointex());
     160      call bar_replaceSegmentFromArray(new_d,i+oneintex(),a_size,a.data,i);
     161      a.data = new_d;
     162    else // Insert in existing array. Appends the new element and shifts the elements to place.
     163      var new_d = a.data;
     164      // Append new element to the end of the array.
     165      call bar_replaceSegment(new_d,a.size,a_size,e);
     166      // Rotate latter part to move into right position
     167      call bar_shiftSegmentGroups(new_d,a_size-i,oneintex(),a_size-i-oneintex(),i,a_size);
     168      a.data = new_d;
     169    end;
     170    a.size = a_size;
     171  };
     172
     173  /** Replace the elements within the given bounds {@code low .. high-1} to the argument value {@code e}. */
    132174  procedure replaceSegment ( upd a:A, obs low:Intex, obs high:Intex, obs e:E )
    133     guard zerointex() <= low && accessible(a,high) && getSize(a) != maximumintex() {
    134     call bar_replaceSegment(a.data,low,high,e);
     175    guard low <= getSize(a) && getSize(a) != maximumintex()
     176  { if high <= bar_getSize(a.data)
     177    then
     178      var new_d = a.data;
     179      call bar_replaceSegment(new_d,low,high,e);
     180      if a.size < high
     181      then
     182        a.size = high;
     183      end;
     184      a.data = new_d;
     185    else
     186      var new_d = bar_createArray_element(bar_getSize(a.data)+high,e);
     187      call bar_replaceSegmentFromArray(new_d,zerointex(),low,a.data,zerointex());
     188      a.size = high;
     189      a.data = new_d;
     190    end;
    135191  };
    136192
    … …  
    139195   */
    140196  procedure replaceSegment ( upd a1:A, obs low:Intex, obs high:Intex, obs a2:A, obs start:Intex )
    141     guard zerointex() <= low && accessible(a1,high) && accessible(a2,start) && accessible(a2,start+high-low)
    142        && getSize(a1) != maximumintex() && getSize(a2) != maximumintex() {
    143     call bar_replaceSegmentFromArray(a1.data,low,high,a2.data,start);
    144   };
    145        
     197    guard low <= getSize(a) && accessible(a2,start) && accessible(a2,start+high-low)
     198       && getSize(a1) != maximumintex() && getSize(a2) != maximumintex()
     199  { if high <= bar_getSize(a1.data)
     200    then
     201      var new_d = a1.data;
     202      call bar_replaceSegmentFromArray(new_d,low,high,a2.data,start);
     203      if a1.size < high
     204      then
     205        a1.size = high;
     206      end;
     207      a1.data = new_d;
     208    else
     209      var new_d = bar_createArray(bar_getSize(a1.data)+high);
     210      call bar_replaceSegmentFromArray(new_d,zerointex(),low,a1.data,zerointex());
     211      call bar_replaceSegmentFromArray(new_d,low,high,a2.data,start);
     212      a1.size = high;
     213      a1.data = new_d;
     214    end;
     215  };
     216
    146217  /** Reverse the order of the elements within the bounds. */
    147218  procedure reverseSegment ( upd a:A, obs low:Intex, obs high:Intex )
    148     guard zerointex() <= low && accessible(a,high) {
     219    guard zerointex() <= low && accessible(a,high)
     220  {
    149221    if a.size != maximumintex()
    150     then call bar_reverseSegment(a.data,low,high);
     222    then
     223      var new_d = a.data;
     224      call bar_reverseSegment(new_d,low,high);
     225      a.data = new_d;
    151226    end;
    152227  };
    153228 
    154229  /** Reverse the order of the elements. */
    155   procedure reverse ( upd a:A ) {
     230  procedure reverse ( upd a:A )
     231  {
    156232    if a.size != maximumintex()
    157     then call bar_reverseSegment(a.data,zerointex(),a.size);
     233    then
     234      var new_d = a.data;
     235      call bar_reverseSegment(new_d,zerointex(),a.size);
     236      a.data = new_d;
    158237    end;
    159238  };
    160239 
    161240  /** Circularly shifts elements a distance @code{d} within the array. */
    162   procedure shift ( upd a:A, obs d:Intex ) {
     241  procedure shift ( upd a:A, obs d:Intex )
     242  {
    163243    if a.size != maximumintex()
    164     then call bar_shiftSegmentGroups(a.data,a.size,oneintex(),a.size-d%a.size,zerointex(),a.size);
    165     end;
    166   };
    167 
    168   /** Obsolete: Splits the array into segments of length {@code k},
    169    * and within each segment, circularly shifts elements a distance @code{d}.
    170    */
    171   procedure shiftElements ( upd a:A, obs d:Intex, obs k:Intex )
    172     guard isSegmentIndex(a,k,oneintex()) && getSize(a) != maximumintex() {
    173     assert idiv(a.size,k)*k == a.size;
    174     assert isSegmentIndex(a,k,idiv(a.size,k));
    175     call bar_shiftSegmentGroups(a.data,k,oneintex(),k-d%k,zerointex(),a.size);
    176   };
    177  
     244    then
     245      var new_d = a.data;
     246      call bar_shiftSegmentGroups(new_d,a.size,oneintex(),a.size-d%a.size,zerointex(),a.size);
     247      a.data = new_d;
     248    end;
     249  };
     250
    178251  /** Circularly left shifts {@code groupsize} size groups of array elements
    179252   * within {@code segsize} size segments of array elements.
    180253   */
    181   procedure shiftSegmentGroups( upd a : A, obs segsize : Intex, obs groupsize : Intex, obs d : Intex ) {
    182     call bar_shiftSegmentGroups(a.data,segsize,groupsize,d,zerointex(),a.size);
    183   };
    184 
    185   /** Obsolete: Splits the array into segments of length {@code k},
    186    * and circularly shifts the segments a distance @code{d}.
    187    */
    188   procedure shiftSegments ( upd a:A, obs d:Intex, obs k:Intex )
    189     guard isSegmentIndex(a,k,oneintex()) && getSize(a) != maximumintex() {
    190     assert idiv(a.size,k)*k == a.size;
    191     assert isSegmentIndex(a,k,idiv(a.size,k));
    192     call bar_shiftSegmentGroups(a.data,a.size,k,idiv(a.size,k)-d%idiv(a.size,k),zerointex(),a.size);
     254  procedure shiftSegmentGroups( upd a : A, obs segsize : Intex, obs groupsize : Intex, obs d : Intex )
     255  { var new_d = a.data;
     256    call bar_shiftSegmentGroups(new_d,segsize,groupsize,d,zerointex(),a.size);
     257    a.data = new_d;
    193258  };
    194259   
    … …  
    259324    if size < maximumintex()
    260325    then
    261       if a.size == maximumintex()
    262       then a.data = bar_createArray(size,bar_getElement(a.data,zerointex()));
    263       end;
    264       call bar_mapf(a.data, a2, c, zerointex(), size);
     326      var new_d =
     327        if a.size == maximumintex()
     328        then bar_createArray(size,bar_getElement(a.data,zerointex()))
     329        else a.data
     330        end;
     331      call bar_mapf(new_d, a2, c, zerointex(), size);
    265332      a.size = size;
     333      a.data = new_d;
    266334    else
    267335      // Assume both arrays are isotropic if their sizes are maximum.
    268336      assert size == maximumintex();
    269337      // This is wrong if the index argument to f is not a dummy.
    270       call bar_mapf(a.data, a2, c, zerointex(), oneintex());
     338      var new_d = a.data;
     339      call bar_mapf(new_d, a2, c, zerointex(), oneintex());
     340      a.data = new_d;
    271341    end;
    272342  };
    … …  
    307377  extend boundedArrayRawCxxPrefix[ bar_simplify_renaming ];
    308378
    309   procedure scan ( upd a:A ) guard getSize(a) != maximumintex() = {
    310     call bar_scan(a.data,zerointex(),a.size);
     379  procedure scan ( upd a:A ) guard getSize(a) != maximumintex()
     380  { var new_d = a.data;
     381    call bar_scan(new_d,zerointex(),a.size);
     382    a.data = new_d;
    311383  };
    312384} [ star => star, scan => scan, bar_scan => bar_scan ]

  • trunk/magnolia-basic-library/src/BasicCxxExamples/LoopsCxxDemo.mg

    r1454 r1576  
    1414
    1515
    16 satisfaction whileTest = {
     16satisfaction whileTestCxx = {
    1717  use boundedNatural32bitCxx;
    1818  use whileLoopCxx
    … …  
    5353 * Running whileTest, untilTest, breakTest, kaerbTest on the same arguments should yield the same results.
    5454 */
    55 satisfaction conditionalLoopTests = {
     55satisfaction conditionalLoopTestsCxx = {
    5656  extend boundedNatural32bitCxx;
    5757  use singletonTuple[T=>Unit];
    … …  
    6666    /** Adapting the requirements to the use context */
    6767    [ Data => Integer, Context => Unit,
    68       cond => cond, body => body
     68      cond => cond, body => p
    6969    ]
    7070    /** Entities defined by the implementation, rename for the using context. */
    … …  
    7575    /** Adapting the requirements to the use context */
    7676    [ Data => Integer, Context => Unit,
    77       body => body, cond => ncond
     77      body => p, cond => ncond
    7878    ]
    7979    /** Entities defined by the implementation, rename for the using context. */
    … …  
    122122
    123123/** Testing the for loop: Functions to double a number many times. */
    124 satisfaction countLoopTest_double = {
     124satisfaction countLoopTest_doubleCxx = {
    125125  use boundedNatural32bitCxx;
    126126  use singletonTuple[T=>Unit];
    … …  
    129129  procedure double(upd n:Integer, obs m:Unit) { n = n+n; };
    130130 
    131   /** The repeat function doubles a number n m times. */
    132   use countLoopCxx[Data => Integer, Context => Unit, p => double ][counter_to_finite];
     131  /** The repeat m times the function {@link double} n. */
     132  use countLoopCxx[Data => Integer, Context => Unit, body => double ][counter_to_finite];
    133133
    134134  /** Calls the repeat statement which should count up to the number m. */
    … …  
    144144
    145145/** Testing the for loop: Define functions to raise a number n to the power of m. */
    146 satisfaction countLoopTest_raise = {
     146satisfaction countLoopTest_raiseCxx = {
    147147  use torusInteger64bitCxx;
    148148
    … …  
    177177/** Testing the for loop: Summation and product of consequtive numbers.
    178178 */
    179 satisfaction countLoopIndexedTest_productAndSum = {
     179satisfaction countLoopIndexedTest_productAndSumCxx = {
    180180  use boundedInteger64bitCxx;
    181181  use singletonTuple[T=>Unit];

  • trunk/magnolia-basic-library/src/BasicCxxRaw/RepetitionCountCxxRawTest.mg

    r1454 r1576  
    1414
    1515/** Testing the for loop: Functions to double a number many times. */
    16 satisfaction repetitionTest = {
     16satisfaction test_repetitionCxx = {
    1717  use adHocPredicateRawInternalCxx;
    1818  use torusInteger8bitCxx[finite_to_small];
    … …  
    2424    /** Adapting the requires part to the use context */
    2525    [ Data => Small, Context => Small,
    26       body => q, body1 => q1, body2 => q2,
     26      body => q,
    2727      Counter => Integer, successorC => successor, zeroc => zero,
    2828      Integer => Integer, successor => successor,
    … …  
    3939    /** Adapting the requires part to the use context */
    4040    [ Data => Small, Context => Small,
    41       body => r, body1 => r1, body2 => r2,
     41      body => r,
    4242      Counter => Integer, successorC => successor, zeroc => zero,
    4343      Integer => Integer, successor => successor,
    … …  
    109109 * - Summation of consequtive numbers.
    110110 */
    111 program powerProductSum = {
     111program test_powerProductSumCxx = {
    112112  use adHocPredicateRawInternalCxx;
    113113  use torusInteger16bitCxx;
    … …  
    136136
    137137  /** Multiplies current value with base value. */
    138   procedure manipulateRaise(upd n:Pair, obs c : Unit, out preempt : Predicate, obs i : Integer) { n.current = n.current * n.base; };
     138  procedure manipulateRaise(upd n:Pair, obs c : Unit, out preempt : Predicate, obs i : Integer) {
     139    var current = n.current * n.base;
     140    n.current = current;
     141  };
    139142 
    140143  procedure successor(upd i : Integer) = { i = i + one(); };
    … …  
    145148    /** Adapting the requires part to the use context */
    146149    [ Data => Pair, Context => Unit,
    147       body => manipulateRaise, body1 => manipulateRaise1, body2 => manipulateRaise2,
     150      body => manipulateRaise,
    148151      Counter => Counter, successorC => successorC, zeroc => zeroc,
    149152      Integer => Integer, successor => successor,
    … …  
    158161    /** Adapting the requires part to the use context */
    159162    [ Data => Integer, Context => Unit,
    160       body => manipulateAdd, body1 => manipulateAdd1, body2 => manipulateAdd2,
     163      body => manipulateAdd,
    161164      Counter => Counter, successorC => successorC, zeroc => zeroc,
    162165      Integer => Integer, successor => successor,
    … …  
    171174    /** Adapting the requires part to the use context */
    172175    [ Data => Integer, Context => Unit,
    173       body => manipulateMultiply, body1 => manipulateMultiply1, body2 => manipulateMultiply2,
     176      body => manipulateMultiply,
    174177      Counter => Counter, successorC => successorC, zeroc => zeroc,
    175178      Integer => Integer, successor => successor,

  • trunk/magnolia-basic-library/src/BasicGeneral/ArrayFilterCxxDemo.mg

    r1454 r1576  
    2626
    2727/** Finding specific elements in an array. */
    28 satisfaction dynamicArrayFloatCxx_findElementIndex_models_ArrayfindElementIndex = {
     28satisfaction test_dynamicArrayFloatCxx_findElementIndex_models_ArrayfindElementIndexCxx = {
    2929  extend dynamicArrayFloatCxx;
    3030  use countLoopIndexedCxx
    … …  
    4040
    4141/** Finding elements smaller than a given value. */
    42 satisfaction dynamicArrayFloatCxx_arrayFindPropertyIndex_models_ArrayFindPropertyIndex = {
     42satisfaction test_dynamicArrayFloatCxx_arrayFindPropertyIndex_models_ArrayFindPropertyIndexCxx = {
    4343  extend dynamicArrayFloatCxx;
    4444  use countLoopIndexedCxx

  • trunk/magnolia-basic-library/src/BasicGeneral/IntegerOperations.mg

    r1454 r1576  
    348348  procedure pp_body( upd d:pp_Data, c:pp_Context ){
    349349    assert zero() < d.n;
    350     if d.n % (one()+one()) != zero()
     350    var n = d.n;
     351    var ret = d.ret;
     352    var x = d.x;
     353    if n % (one()+one()) != zero()
    351354    then
    352       d.n = d.n - one();
    353       d.ret = star(d.ret,d.x);
     355      d.n = n - one();
     356      d.ret = star(ret,x);
    354357    end;
    355       d.n = idiv(d.n, one()+one());
     358      d.n = idiv(n, one()+one());
    356359      if d.n != zero()
    357       then d.x = star( d.x, d.x);
     360      then d.x = star( x, x);
    358361      end;
    359362  };
    360  
     363
    361364  /** The predicate that must hold. */
    362365  predicate pp_cond( d:pp_Data, c:pp_Context ) = zero() < d.n;

  • trunk/magnolia-basic-library/src/Makefile

    r1556 r1576  
    111111        BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal roundingAxioms -- -4.5
    112112        BasicCxx/FloatCxx/float32bitCxx_is_FiniteReal transitive 6.7 6.7 6.7
    113         BasicCxx/FloatCxx/float80bitCxx_is_FiniteReal naturalLogarithmAxiom1 3
    114         BasicCxx/FloatCxx/float80bitCxx_is_FiniteReal naturalLogarithmAxiom1 0
     113        BasicCxx/FloatCxx/float80bitCxx_is_FiniteReal naturalLogarithmAxiom
     114        BasicCxx/FloatCxx/float80bitCxx_is_FiniteReal naturalLogarithmPowAxiom 3
     115        BasicCxx/FloatCxx/float80bitCxx_is_FiniteReal naturalLogarithmPowAxiom 1
    115116        TutorialExamples/Tutorial9Cxx/fibonacciLookuptable_provides_FibonacciCxx fibtable > fibtable.Fibtable &&\
    116117          test `TutorialExamples/Tutorial9Cxx/fibonacciExternalCxx fib -i1 fibtable.Fibtable  27` -eq 196418

  • trunk/magnolia-basic-library/src/Mathematics/Numbers.mg

    r1454 r1576  
    569569    assert log(one()) == zero();
    570570  }
    571   axiom naturalLogarithmAxiom ( x:Number ) {
     571  axiom naturalLogarithmPowAxiom ( x:Number ) {
    572572    assert pow(e(),x) == exp(x);
    573573  }

  • trunk/magnolia-basic-library/src/TutorialExamples/Tutorial0Cxx.mg

    r1555 r1576  
    66 * Suffix Cxx implies that it may be possibly to compile the modules to executable C++ code.
    77 *
    8  * @author Jaakko Jarvi, Magne Haveraaaen
     8 * @author Jaakko JÀrvi, Magne Haveraaaen
    99 * @since 2015-03-17
    1010 */
    … …  
    3535program welcomeCxx = { // Named program: suffix Cxx indicates programming language for target.
    3636 
    37   /** Uses the string module, with {@code concatenate} written as infix {@code *}. */
     37  /** Uses the string module, with {@code concatenate} and {@code createEmptyString} functions. */
    3838  use stringCxx;
    3939  /** Uses the string module defining the latin characters, digits and more. */

  • trunk/magnolia-basic-library/src/TutorialExamples/Tutorial3Cxx.mg

    r1476 r1576  
    1717imports
    1818  BasicCxx.IntegerCxx,
    19   BasicCxx.FloatCxx;
     19  BasicCxx.FloatCxx,
     20  BasicCxx.StringCxx;
    2021
    2122/** An implementation of 3 functions
    … …  
    6162};
    6263
     64program strenging = {
     65  use stringCxx;
     66  use recurring
     67    [ T => String, binop => concatenate ]
     68    [ once => square, twice => cube, thrice => tesseract ];
     69};
    6370
    6471/** Creating a simple implementation by combining implementations.
    … …  
    111118    [ once => max1, twice => max2, thrice => max3 ];
    112119
     120  function min5 ( a:Float, b:Float, c:Float, d:Float, e:Float ) : Float
     121  = min(min(min(a,b),min(b,c)),e);
     122
    113123  /** Uses recurring directly on the power function.
    114124   * Notice how fast the function grows.

  • trunk/magnolia-basic-library/src/TutorialExamples/Tutorial4Cxx.mg

    r1454 r1576  
    3131   echo 12 > i7.Integer ; cp v1.MY v2.MY
    3232   TutorialExamples/Tutorial4Cxx/gradual25integersCxx st -io1 i7.Integer -io2 v2.MY && head v2.MY i7.Integer
    33 //TODO   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY -i2 v1.MY 99
    34 //TODO   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY -i2 v1.MY -- -5678
    35 //TODO   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY '<Mytype#Integer.Integer>4 20480</Mytype#Integer.Integer> 66
    36 //TODO   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY '<Mytype#Integer.Integer>4 2</Mytype#Integer.Integer>' -- -44
     33   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY -i2 v1.MY 99
     34   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY -i2 v1.MY -- -5678
     35   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY '<Mytype#Integer.Integer>4 20480</Mytype#Integer.Integer>' 66
     36   TutorialExamples/Tutorial4Cxx/gradual25integersCxx big -i1 v1.MY '<Mytype#Integer.Integer>4 2</Mytype#Integer.Integer>' -- -44
    3737 * </pre>
    3838 * Note the use of "-ioN" for updatable procedure arguments.
    39  * Also note that we can change the output to go directly to the terminal by using "-iN" for the argument.
     39 * Also note that we can change the output to go directly to the terminal by using "-iN" for the argument
     40 * in a procedure with a single update argument.
    4041 * <pre>
    4142   TutorialExamples/Tutorial4Cxx/gradual25integersCxx increase -i1 v1.MY
    … …  
    5657/** An implementation of types, functions, procedures and predicates.
    5758 * NB! Magnolia does not support recursion, neither directly nor indirectly.
     59 * NB! There are no loop constructs in the Magnolia language, but they are provided in the library.
    5860 */
    5961implementation example = {
    … …  
    7072  type Mytype = struct{ var left:T; var right:T; };
    7173 
     74  /** Defining a function that creates a data value of the record type {@link Mytype} using its constructor. */
    7275  function build (a:T, b:T) : Mytype = Mytype{ left = a, right = binop(a,b) };
    7376 
    74   /** This procedure induces one function:
     77  /** In Magnolia procedure induces set of functions corresponding to
     78   * the same information flow as the procedure.
     79   * An induced function is used and behaves exactly like a normal function.
     80   * In this case, the procedure induces exactly one function:
    7581   *    function increase(x : Mytype) : Mytype;
    76    * An induced function works exactly as a normal function.
    7782   */
    7883  procedure increase ( upd x:Mytype ) = {
     84    /* Here we access the components of the record type {@link Mytype} using the "dot" notation. */
     85    var xl = x.left;
    7986    if x.left == x.right
    80     then x.left = binop(x.left,x.left);
     87    then xl = binop(x.left,x.left);
    8188    else skip;
    8289    end;
    83     x.right = binop(x.left,x.right);
     90    x.left = xl;
     91    var xr = x.right;
     92    x.right = binop(xl,xr);
    8493  };
    8594 
    86   /** NOTE: the error message here is a compiler feature, not an error in the code. */
     95  /** Defining a function as a value block. */
    8796  function bigger ( x:Mytype ) : T = {
    8897    var t:T = x.left;
    … …  
    92101  };
    93102 
    94   /** A predicate. */
     103  /** A predicate defined by a simple expression. */
    95104  predicate small ( a:Mytype ) = a.left <= a.right;
    96105
    … …  
    105114  };
    106115
    107 /*< TODO: code temporarily removed due to a compiler error: nested function blocks are not supported correctly.
    108   /** A trinary predicate. */
     116  /** A trinary predicate defined by nested value blocks.
     117   * The inner block block defines a value which is used in the outer block.
     118   * TODO! The Magnolia compiler does not generate correct code for an inner value block!
     119   */
    109120  predicate big ( a:Mytype, b:Mytype, c:T ) = {
    110121    var t:T = binop(a.left,b.right);
    … …  
    119130      end && a != b;
    120131  };
    121 >*/
     132
    122133 
    123134};

  • trunk/magnolia-basic-library/src/TutorialExamples/Tutorial9Cxx.mg

    r1457 r1576  
    1313 *   {@link fibonacciRoundingSimple}: the implementation has trimmed down the requirements to a minimum.
    1414 * - {@link fibonacciIteration}: using counted loops ("for loop") to iterate to the n'th number in O(n) steps.
    15  * - {@link fibonacciLookuptable}: computes (using for loops) an array with all Fibonacci numbers representable in 64bit numbers,
    16  *   then looks up the the n'th Fibunacci number in the table.
    17  * - {@link fibonacciExternalCxx}: reads in a table of Fibunacci numbers and looks up the actual number.
     15 * - {@link fibonacciLookuptable}: computes (using for loops) an array with all Fibonacci numbers representable in 64bit natural numbers,
     16 *   then looks up the the n'th Fibonacci number in the table.
     17 * - {@link fibonacciExternalCxx}: reads in a table of Fibonacci numbers and looks up the actual number.
    1818 *
    1919 * @see https://en.wikipedia.org/wiki/Fibonacci_number
    … …  
    8181 * There are two distinct implementations:
    8282 * - {@link fibonacciRoundingFloat} which is entirely float based, even the IO, though only integral values can be used.
    83  *   This implementation will approximate the Fibonacci numbers when the numbers become to big to be represented exactly,
    84  *   but it fails quite early due to representation errors in the golden ratio.
     83 *   This implementation will approximate the Fibonacci numbers when the numbers become too big to be represented exactly,
     84 *   but it fails the axioms quite early due to representation errors in the golden ratio.
    8585 * - {@link fibonacciRounding} adds a conversion from (argument values) and to integers (result value) for the Fibonacci function.
    8686 *   It has the same inaccuracy problems as {@link fibonacciRoundingFloat},
    8787 *   but will only return the maximum representable integer when the Fibonacci number goes out of range.
    88  *   The implementation {@link fibonacciRoundingSimple} is a variation of this,
     88 * - The implementation {@link fibonacciRoundingSimple} is a variation of {@link fibonacciRounding},
    8989 *   where the requirements have been trimmed as much as possible from using full library modules.
    9090 *
    … …  
    9595 *   since the properties of the premises are needed to prove the claim.
    9696 * - An executable claim (that we approcximate the Fibonacci function),
    97  *   {@link fibonacciRoundingFloat64_provides_FibonacciCxx},
    98  *   {@link fibonacciRounding64_provides_FibonacciCxx} and {@link fibonacciRounding80_provides_FibonacciCxx}.
     97 *   {@link fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci},
     98 *   {@link fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci} and {@link fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci}.
    9999 *   These uses executable approximations (finite floats) without complete specifications for the premises,
    100100 *   hence the implementations can only be tested and not proven correct.
    101  *   Also we should expect some approximation to the correct result for many of the arguments.
     101 *   We expect approximations to the correct result for all of the arguments.
    102102 *
    103103 * Run the following command to check the axioms for the first 100 Fibonacci numbers using the executable satisfactions.
    104104 * <pre>
    105    for file in TutorialExamples/Tutorial9Cxx/fibonacciRounding*Cxx
     105   for file in TutorialExamples/Tutorial9Cxx/fibonacciRounding*Cxx*_provides_Fibonacci
    106106   do echo $file
    107107      $file fibonacciBaseAxiom
    108       for i in {0,1,2,3,4,5,6,7,8,9}{0,1,2,3,4,5,6,7,8,9}
     108      for i in {0..100}
    109109      do $file fibonacciGeneralAxiom $i || echo $i
    110110      done
    … …  
    147147 * The inaccuracies in the representation of floating point numbers causes errors in the last digits already of {@code fib(71)},
    148148 * Which has a value significantly below the maximum exactly representable integer in 64 bit floating point.
    149  * On the other hand, we may get approximate values for large values of fib, up to {@code fib(71)==1.9068715787994046392e+307}.
    150  * <pre>
    151    TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat64_provides_FibonacciCxx fibonacciGeneralAxiom 71
    152    TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat64_provides_FibonacciCxx integer_maximum
    153    TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat64_provides_FibonacciCxx fib 71
    154    TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat64_provides_FibonacciCxx fib 1472
    155  * </pre>
    156  */
    157 satisfaction fibonacciRoundingFloat64_provides_FibonacciCxx =
     149 * On the other hand, we may get approximate values for large values of fib, up to {@code fib(1474)==4.9922546054780146353e+307}.
     150 * <pre>
     151   TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci fibonacciGeneralAxiom 71
     152   TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci integer_maximum
     153   TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci fib 71
     154   TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci fib 93
     155   TutorialExamples/Tutorial9Cxx/fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci fib 1474
     156 * </pre>
     157 */
     158satisfaction fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci =
    158159  float64bitCxx
    159160with fibonacciRoundingFloat
    … …  
    248249/**
    249250 * Providing a test setup using 64 bit floats and 64 bit natural numbers for {@link fibonacciRoundingSimple}.
    250  * We see the same inaccuracies as for {@link fibonacciRoundingFloat64_provides_FibonacciCxx},
     251 * We see the same inaccuracies as for {@link fibonacciRoundingFloat_float64bitCxx_provides_Fibonacci},
    251252 * i.e., {@code fib(71)} also has an error in the last digit.
    252253 * However, the conversion to integers means we cannot approximate large values of fib.
    … …  
    254255 * which deviates from the correct result 12200160415121876738 in the last 6 digits.
    255256 * Note that in this approximation {@code fib(93)==fib(92)+fib(91)}, even though the answer is wrong,
    256  * it just happens to be the case that the computation errors coinside with the assertion.
     257 * it just happens to be the case that the computation errors of those 3 fibonacci numbers coinside with the assertion.
    257258 * Any higher Fibonacci number flattens out at 18446744073709551615, the highest natural number represented by 64 bits.
    258259 * This is a property of {@link conversionRealIntegerApproximateCxx}.
    … …  
    260261 *
    261262 * <pre>
    262    TutorialExamples/Tutorial9Cxx/fibonacciRounding64_provides_FibonacciCxx fibonacciGeneralAxiom 71
    263    TutorialExamples/Tutorial9Cxx/fibonacciRounding64_provides_FibonacciCxx integer_maximumf
    264    TutorialExamples/Tutorial9Cxx/fibonacciRounding64_provides_FibonacciCxx maximumi
    265    TutorialExamples/Tutorial9Cxx/fibonacciRounding64_provides_FibonacciCxx fib 71
    266    TutorialExamples/Tutorial9Cxx/fibonacciRounding64_provides_FibonacciCxx fib 93
    267    TutorialExamples/Tutorial9Cxx/fibonacciRounding64_provides_FibonacciCxx fibonacciGeneralAxiom 93
    268    TutorialExamples/Tutorial9Cxx/fibonacciRounding64_provides_FibonacciCxx fib 94
    269  * </pre>
    270  */
    271 satisfaction fibonacciRounding64_provides_FibonacciCxx = {
     263   TutorialExamples/Tutorial9Cxx/fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci fibonacciGeneralAxiom 71
     264   TutorialExamples/Tutorial9Cxx/fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci integer_maximumf
     265   TutorialExamples/Tutorial9Cxx/fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci maximumi
     266   TutorialExamples/Tutorial9Cxx/fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci fib 71
     267   TutorialExamples/Tutorial9Cxx/fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci fib 93
     268   TutorialExamples/Tutorial9Cxx/fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci fibonacciGeneralAxiom 93
     269   TutorialExamples/Tutorial9Cxx/fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci fib 94
     270 * </pre>
     271 */
     272satisfaction fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci = {
    272273  use float64bitCxx[ float_to_suffix_f ];
    273274  use conversionRealIntegerApproximateCxx;
    274275  use boundedNatural64bitCxx[ integer_to_suffix_i ];
    275 } with fibonacciRoundingSimple
     276} with fibonacciRounding
    276277approximates Fibonacci[ integer_to_suffix_i ];
    277278
    278279/**
    279  * Providing a test setup using 80 bit floats and 64 bit natural numbers for {@link fibonacciRoundingSimple}.
    280  * The inaccuracies are similar to {@link fibonacciRounding64_provides_FibonacciCxx},
     280 * Providing a test setup using 80 bit floats and 65 bit integers for {@link fibonacciRoundingSimple}.
     281 * The inaccuracies are similar to {@link fibonacciRounding_float64bitCxx_boundedNatural64bitCxx_provides_Fibonacci},
    281282 * but have been postponed to {@code fib(79)==14472334024676222} which has an error in the last digit.
    282283 * The largest Fibonacci number we can approximate reasonably well still is {@code fib(93)==12200160415121876992},
    283284 * which now deviates from the correct result 12200160415121876738 only in the last 3 digits.
    284285 * <pre>
    285    TutorialExamples/Tutorial9Cxx/fibonacciRounding80_provides_FibonacciCxx fibonacciGeneralAxiom 79
    286    TutorialExamples/Tutorial9Cxx/fibonacciRounding80_provides_FibonacciCxx integer_maximumf
    287    TutorialExamples/Tutorial9Cxx/fibonacciRounding80_provides_FibonacciCxx maximumi
    288    TutorialExamples/Tutorial9Cxx/fibonacciRounding80_provides_FibonacciCxx fib 79
    289    TutorialExamples/Tutorial9Cxx/fibonacciRounding80_provides_FibonacciCxx fib 93
    290    TutorialExamples/Tutorial9Cxx/fibonacciRounding80_provides_FibonacciCxx fib 94
    291  * </pre>
    292  */
    293 satisfaction fibonacciRounding80_provides_FibonacciCxx = {
     286   TutorialExamples/Tutorial9Cxx/fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci fibonacciGeneralAxiom 79
     287   TutorialExamples/Tutorial9Cxx/fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci integer_maximumf
     288   TutorialExamples/Tutorial9Cxx/fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci maximumi
     289   TutorialExamples/Tutorial9Cxx/fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci fib 79
     290   TutorialExamples/Tutorial9Cxx/fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci fib 93
     291   TutorialExamples/Tutorial9Cxx/fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci fib 94
     292   TutorialExamples/Tutorial9Cxx/fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci fib 1474
     293 * </pre>
     294 */
     295satisfaction fibonacciRoundingSimple_float80bitCxx_boundedInteger65bitCxx_provides_Fibonacci = {
    294296  use float80bitCxx[ float_to_suffix_f ];
    295297  use conversionRealIntegerApproximateCxx;
    … …  
    313315   do echo $file
    314316      $file fibonacciBaseAxiom
    315       for i in {0,1,2,3,4,5,6,7,8,9}{0,1,2,3,4,5,6,7,8,9}
     317      for i in {0..99}
    316318      do $file fibonacciGeneralAxiom $i || echo $i
    317319      done
    … …  
    351353   */
    352354  procedure body( upd d:Pair, obs c:Integer ) {
    353     var f = d.f1 + d.f2;
    354     d.f2 = d.f1;
     355    var p = d;
     356    var f = p.f1 + p.f2;
     357    d.f2 = p.f1;
    355358    d.f1 = f;
    356359  }
    … …  
    407410   do echo $file
    408411      $file fibonacciBaseAxiom
    409       for i in {0,1,2,3,4,5,6,7,8,9}{0,1,2,3,4,5,6,7,8,9}
     412      for i in {0..99}
    410413      do $file fibonacciGeneralAxiom $i || echo $i
    411414      done
    … …  
    415418 */
    416419
    417 /** The Fibonacci function implemented by creating a lookup table with 93 entries and then using this.
    418  * Computing Fibonacci for 93 requires at least 64 bit natural numbers.
     420/** The Fibonacci function implemented by creating a lookup table with entries including fib(93).
     421 * Computing Fibonacci for 94 requires more than 64 bit natural numbers.
    419422 *
    420423 * The implementation first fills an array Fibtable with the Fibonacci numbers starting the base cases 0 and 1,
    … …  
    444447  }
    445448 
    446   /** Function that creates a {@link Fibtable} for the given number of entries. */
     449  /** Function that creates a {@link Fibtable} for Fibonacci numbers 0..n. */
    447450  function initialiseFibtable( n:Intex ) : Fibtable =
    448     /** Compute the table of Fibonacci numbers for entries i+1 for i=1,..,n-1. */
     451    /** Compute the table of Fibonacci numbers for entries i+1 for i=1,..,n. */
    449452    repeat(
    450453      /** Change the first element of the array to 1, ensuring the base case is corrrectly stored in the Fibonacci array. */
    451454      change(
    452         /** Initialise an array og n+1 elements, all being 0. */
     455        /** Initialise an array of n+1 elements, all being 0. */
    453456        createArray(n+I(),zerointex()),
    454457        I(),
    … …  
    463466    );
    464467 
    465   /** A constant {@link Fibtable} with 93 entries - as much as possible for {@code long int}. */
     468  /** A constant {@link Fibtable} with entries for fib(0)..fib(93) - all possible fibonacci entries for 64 bit natural numbers. */
    466469  function fibtable () : Fibtable = initialiseFibtable(L() + XL() + III());
    467470 
    … …  
    471474
    472475/**
    473  * Providing a test setup using 64 bit integers ({@code size_t}) since this allows Fibonacci numbers up to 93.
     476 * Providing a test setup using 64 bit natural numbers ({@code size_t} in C++ for 64bit architectures)
     477 * which allows Fibonacci numbers up to 93.
    474478 * For argument 94 the lookup function obviously fails.
    475479 */
    … …  
    492496   for file in TutorialExamples/Tutorial9Cxx/fibonacciExternalCxx
    493497   do echo $file
    494       for i in {0,1,2,3,4,5,6,7,8,9}{0,1,2,3,4,5,6,7,8,9}
     498      for i in {0..99}
    495499      do echo -n $i ' ' ; $file fib -i1 fibtable.Fibtable $i
    496500      done
Note: See TracChangeset for help on using the changeset viewer.