Predicative programming
પ્રેડીકેટિવ પ્રોગ્રામિંગ એ પ્રોગ્રામ સ્પષ્ટીકરણ અને શુદ્ધિકરણ માટેની ઔપચારિક પદ્ધતિનું મૂળ નામ છે, જેને તાજેતરમાં એરિક હેનર દ્વારા શોધાયેલ પ્રેક્ટિકલ થિયરી ઓફ પ્રોગ્રામિંગ તરીકે ઓળખવામાં આવે છે. કેન્દ્રિય વિચાર એ છે કે દરેક સ્પષ્ટીકરણ દ્વિસંગી (બુલિયન) અભિવ્યક્તિ છે જે સ્વીકાર્ય કમ્પ્યુટર વર્તણૂકો માટે સાચું છે અને અસ્વીકાર્ય વર્તણૂકો માટે ખોટું છે. તે અનુસરે છે કે શુદ્ધિકરણ એ માત્ર સૂચિતાર્થ છે. આ સૌથી સરળ ઔપચારિક પદ્ધતિ છે, અને સૌથી સામાન્ય છે, જે ક્રમિક, સમાંતર, એકલ, સંદેશાવ્યવહાર, સમાપ્તિ, બિન-સમાપ્તિ, કુદરતી-સમય, વાસ્તવિક-સમય, નિર્ધારક અને સંભવિત કાર્યક્રમો પર લાગુ થાય છે, અને તેમાં સમય અને અવકાશની સીમાઓનો સમાવેશ થાય છે. પ્રોગ્રામિંગ ભાષામાં આદેશોને સ્પષ્ટીકરણનો એક વિશેષ કેસ માનવામાં આવે છે-તે સ્પષ્ટીકરણો કે જે સંકલનક્ષમ હોય છે. ઉદાહરણ તરીકે, જો પ્રોગ્રામ વેરિયેબલ્સ છે, અને, આદેશઃ = + 1 એ સ્પષ્ટીકરણ (દ્વિસંગી અભિવ્યક્તિ) = + 1 ¥ = ¥ = ની સમકક્ષ છે, જેમાં, અને સોંપણી પહેલાં પ્રોગ્રામ વેરિયેબલ્સના મૂલ્યોનું પ્રતિનિધિત્વ કરે છે, અને, અને સોંપણી પછી પ્રોગ્રામ વેરિયેબલ્સના મૂલ્યોનું પ્રતિનિધિત્વ કરે છે. જો સ્પષ્ટીકરણ> હોય, તો આપણે સરળતાથી (: = + 1) ુણ (>) સાબિત કરીએ છીએ, જે કહે છે કેઃ = + 1 સૂચવે છે, અથવા સુધારે છે, અથવા અમલ કરે છે. લૂપ પ્રૂફ ખૂબ સરળ છે. ઉદાહરણ તરીકે, જો પૂર્ણાંક ચલ હોય, તો તે સાબિત કરવા માટે કે જ્યારે> 0 ડુઃ =-1 ઓડ રિફાઈન્સ કરે છે, અથવા સ્પષ્ટીકરણનો અમલ કરે છે, ત્યારે સાબિત કરો કે> 0 તો પછીઃ =-1; (≤0 િયમ = 0) અન્યથા ફાઈ ણિ (≤0 ણિ = 0) જ્યાં = (=) ખાલી છે, અથવા ડુ-નથિંગ આદેશ છે. લૂપ અપરિવર્તનશીલ અથવા ઓછામાં ઓછા નિશ્ચિત બિંદુની જરૂર નથી. બહુવિધ મધ્યવર્તી છીછરા અને ઊંડા બહાર નીકળતા લૂપ્સ એ જ રીતે કામ કરે છે. સાબિતીનું આ સરળ સ્વરૂપ શક્ય છે કારણ કે પ્રોગ્રામ આદેશો અને સ્પષ્ટીકરણોને અર્થપૂર્ણ રીતે એકસાથે મિશ્રિત કરી શકાય છે. અમલનો સમય (ઉપલી સીમાઓ, નીચલી સીમાઓ, ચોક્કસ સમય) એ જ રીતે સાબિત કરી શકાય છે, માત્ર સમય ચલ રજૂ કરીને. સમાપ્તિ સાબિત કરવા માટે, અમલનો સમય મર્યાદિત છે તે સાબિત કરો. બિનસમાપ્તિ સાબિત કરવા માટે, અમલનો સમય અનંત છે તે સાબિત કરો. ઉદાહરણ તરીકે, જો સમય ચલ છે, અને સમયને પુનરાવર્તનોની ગણતરી દ્વારા માપવામાં આવે છે, તો પછી તે સાબિત કરવા માટે કે અગાઉના વાઇલ-લૂપના અમલમાં સમય લાગે છે જ્યારે શરૂઆતમાં બિન-નકારાત્મક હોય છે, અને જ્યારે શરૂઆતમાં નકારાત્મક હોય ત્યારે કાયમ લે છે, તો સાબિત કરો કે> 0 તો પછીઃ =-1;: = + 1; (≤0 * = +) ≤ (<0 * = ≤) અન્યથા ≤ (≤0 * = +) ≤ (<0 * = ≤) જ્યાં = (= ≤ =). ગ્રંથસૂચિ ઇ. સી. આર. હેનર, એ પ્રેક્ટિકલ થિયરી ઓફ પ્રોગ્રામિંગ, સ્પ્રિંગર-વેરલેગ 1993. પ્રોગ્રામિંગના પ્રાયોગિક સિદ્ધાંત પર સૌથી તાજેતરની આવૃત્તિ ઓનલાઇન. બાહ્ય કડીઓ એરિક હેનર દ્વારા પ્રકાશનો. ઔપચારિક પદ્ધતિઓ ઔપચારિક સ્પષ્ટીકરણ ભાષાઓ તાર્કિક ગણતરી