Programs: finance

17 verified Soma programs in the finance domain. Each page shows the source and what soma check, soma test, soma verify and soma run printed on it.

Program	Lines	Uses
Fixed-coupon bond pricing: present value of coupons plus redemption, current yield, and a par/premium/discount classifier	49
Monthly budget tracker with a spend cap invariant	54	a memory invariant, try / catch
Chip/cash ledger with a non-negative balance invariant	54	a memory invariant, try / catch
Compound interest: future value, with periodic compounding and a continuous-compounding variant	46
FX converter with a rate table in memory and a non-negative rate invariant	60	a memory invariant, try / catch
Equity income metrics: dividend yield, payout ratio, dividend-discount	49
Brokerage fee calculator: tiered commission, bps fee with a floor, and a maker/taker exchange fee	57	match
Fixed-rate loan amortization: monthly payment, remaining balance after k payments, and total interest paid	48
Moving averages over a price series: simple MA window, full-series mean, and a momentum signal from an SMA crossover	64
Discounted cash flow: present value of a single flow, net present value of a cash-flow stream, and a simple payback-period count	57
European option payoffs at expiry, plus a long straddle	56
Order lifecycle as a verified state machine: an order flows from new to filled or rejected, and a fill settles	63	a state machine, guard blocks
Portfolio P&L tracker over a list of position records	63	pipes (\|>), lambdas
Position-limit risk gate. Each symbol's net position must stay within	59	a memory invariant, try / catch
Return-series statistics: arithmetic mean return, volatility (sample stdev), annualized Sharpe ratio, and max drawdown of an equity curve	62
Progressive income tax over marginal brackets, plus effective rate and marginal rate lookup	70
Trade settlement as a sum type	58	a sum type, match