title: Integer division in awk
body: <p>I want to divide two numbers in <code>awk</code>, using integer division, i.e truncating the result. For example </p>
  
  <pre><code>k = 3 / 2
  print k
  </code></pre>
  
  <p>should print <code>1</code></p>
  
  <p>According to <a href="http://www.gnu.org/software/gawk/manual/html_node/Arithmetic-Ops.html" rel="noreferrer">the manual</a>, </p>
  
  <blockquote>
    <p>Division; because all numbers in awk are floating-point numbers, the result is <strong><em>not rounded to an integer</em></strong></p>
  </blockquote>
  
  <p>Is there any workaround to get an integer value?</p>
  
  <p>The reason is that I want to get the <em>middle element</em> of an array with <em>integer</em> indexes [0 to num-1]. </p>