dadlldate-line

ライブラリ: dadlldataline

function extern concat.fix(
ref string dataline(),
long offset,
const long spos(,),
const long leng(,),
long index, ... )

前 : 
引数リストの可変部分を arg1, ..., argn (n >= 0) とする
これらの引数のタイプを typei (1 <= i <= n) とする

データ行のために予約されているスペースは、結果の格納に十分な長さとする
AND offset >= 1
AND length_of_array(spos) >= n
AND length_of_array(leng) >= n
AND FORALL i: 1 <= i <= length_of_array(spos) : spos(i) >= 1
AND FORALL i: 1 <= i <= length_of_array(leng) : leng(i) >= 0

後 : FORALL i: 1 <= i <= n:
- dataline(offset+spos(i)-1; leng(i)) =
( typei = string ? argi : str$(argi) )
説明 : 上の条件式は、理解しやすさを優先した式であり、正式な書法とは言えません。

問題:
- 引数の重複: 複数の引数に関して結果文字列内で占めるべき場所が重複した場合、上の事後条件は、重複した引数のうちの少なくとも 1 つに対してのみ成立します。
また、引数が文字列に設定される順序は未定義です。
- len(argi) > leng(i) (typei = string) の場合は、argi は切り詰められます。

len(str$(argi)) > leng(i) (typei = numeric) の場合は、str$(argi) は切り詰められます (わずかな精度低下を伴なう可能性があります)。

function extern long scan.fix(
const string dataline(),
ref long offset,
const long spos(,),
const long leng(,),
long index,
long llen, ... )

前 : 
引数リストの可変部分を arg1, ..., argn (n >= 0) とします。
これらの引数のタイプを typei (1 <= i <= n) とします。

offset >= 1
AND length_of_array(spos) = length_of_array(leng) >= n
AND FORALL i: 1 <= i <= n : spos(i) >= 0
AND FORALL i: 1 <= i <= n : leng(i) >= 0
AND FORALL i: 1 <= i <= n : spos(i) = 0 => leng(i) = 0
AND llen = MAX j: 1 <= j <= n : spos(j) + leng(j) - 1
返値: len(line) >= offset + llen - 1 or (len(line) >= offset + spos(n) - 1 and typen = string)

後 : ret ==> FORALL i: 1 <= i <= n and spos(i) > 0:
typei = string ==> argi = dataline(offset+spos(i)-1;leng(i))
typei = double ==> argi = val( ,, )
typei = long ==> argi = lval( ,, )

AND FORALL i: 1 <= i <= n and spos(i) = 0: argi = old(argi)
AND offset = old(offset) + llen
説明: 関数 concat.fix とは対照的に、この関数では引数の重複の問題はありません。
spos の値が 0 のフィールド (複数可) は、変更されたり空にされたりはしません (これは、複数行にわたるフィールドをスキップするためです)。

function extern long scan.sepa(
const string dataline(),
ref long offset,
string sepa(1),
string encl(1), ... )

前 : 引数リストの可変部分を arg1, ..., argn (n >= 0) とします。これらの引数のタイプを typei (1 <= i <= n) とします。

offset >= 1
AND len(sepa) = 1

返値: 値が格納された引数の数 (このため、0 <= retval <= n)

後 : FORALL i: 1 <= i <= retval:
typei = long ==> argi = lval(SUBSTR(i)) AND
typei = double ==> argi = val(SUBSTR(i)) AND
typei = string and (encl = "" or SUBSTR(i) = "") ==> argi = SUBSTR(i) AND
typei = string and encl <> "" ==> argi = SUBSTR(2; len(SUBSTR(i)-2))

offset = old(offset) + SEPA.OCC(retval) - 1

説明 : SUBSTR(i) は次のとおりに定義されます。
dataline(offset+SEPA.OCC(i-1); SEPA.OCC(i)-SEPA.OCC(i-1)-1)
(すなわち、(i-1) 番目の区切りと i 番目の区切りとの間に入るサブ文字列)

および SEPA.OCC は次のとおりに定義されます。
SEPA.OCC(0) = 0
SEPA.OCC(1) = pos(dataline(offset), sepa)
SEPA.OCC(n) = SEPA.OCC(n-1) +
pos(dataline(offset+SEPA.OCC(n-1)), sepa)
(pos の値が正である場合のみ。また、囲み文字の間に区切り文字がある場合を考慮していません。)
SEPA.OCC(m) = len(dataline) - offset + 2
(上記以外の場合)
(すなわち、dataline(offset) での i 番目の区切りの場所、または、区切りが無い場合は文字列終端直後)

こうして、この関数はデータ行を区切り sepa によって複数のサブ文字列に分割します。これらのサブ文字列は各引数に代入されます (必要ならば、変換関数 lval または val を使用して)。offset は、最後に走査されたサブ文字列の後 (または、この最後のサブ文字列に続いて区切りがある場合は、
その区切りの後) に設定されます。
返値は、走査できた引数の個数を示します。このため、上限は以下に挙げる個数となります。
- 可変引数の個数
- dataline に含まれる区切りの個数 (offset の位置以降)

encl <> "" の場合、文字列引数は以下のいずれかです。
- 囲み文字 encl で挟まれている
- 空 (すなわち、2 つの区切りが連続した位置に存在する)
注意： 1 つの文字列を複数のフェーズで走査する場合、
offset は、n 番目の引数の後の区切りの次を示す必要があります。(その区切りではなく)